Loco : Formal Proofs of Local Computation Systems
Description
Loco is a library of Coq theories
devoted to the formal proofs of local computation
systems.
Publications
- Pierre Castéran, Vincent Filou and Mohamed Mosbah
Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant
SCSS 09
- Pierre Castéran and Vincent Filou
Tâches, types et tactiques pour les systès de calculs locaux
J.F.L.A. 2010
- Yves Bertot and Pierre Castéran
The Coq'Art book
(a version in Chinese will be available soon.)
Documentation
Download
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.
Links
the Visidia tool