Loco : Formal Proofs of Local Computation Systems


Loco is a library of Coq theories devoted to the formal proofs of local computation systems.

This project is partially funded by the French Agency Agence Nationale de la Recherche : Projet Impex .




A first draft implementation in Coq8.3, written by Pierre Castéran and Vincent Filou is available here.

This is clearly a work in progress. Many definitions and proofs are too long and are being improved little by little.
A new version, dealing with randomised distributed algorithm will be released in summer 2014. Draft versions can be sent to interested people. It is written by Pierre Castéran and includes graph representation contributed by Allyx Fontaine.


the Visidia tool