Loco : Formal Proofs of Local Computation Systems
Loco is a library of Coq theories
devoted to the formal proofs of local computation
This project is partially funded by the French Agency Agence Nationale de la
Recherche : Projet Impex .
- Pierre Castéran, Vincent Filou and Mohamed Mosbah
Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant
- Pierre Castéran and Vincent Filou
Tâches, types et tactiques pour les systès de calculs locaux
- Yves Bertot and Pierre Castéran
The Coq'Art book
A first draft implementation in Coq8.3, written by
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