Loco : Formal Proofs of Local Computation Systems
Loco is a library of Coq theories
devoted to the formal proofs of local computation
- 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 version in Chinese will be available soon.)
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.
the Visidia tool