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


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