Krivine Nets

Located in the formalisation directory.

Roadmap of main definitions and theorems:
  * Lambda.agda: Source language
  * Krivine.agda: Definition of the Krivine machine constituents and
                  transition relation
  * Krivine/Properties.agda: Krivine is deterministic, termination and
                             divergence for Krivine
  * Network.agda: Synchronous and asynchronous networks
  * DKrivine.agda: Definition of the Distributed Krivine machine constituents
                   and transition relation
  * DKrivine/Properties.agda: point-to-point, DKrivine is deterministic,
                              conversion between asynchronous and synchronous
                              networks, termination and divergence for
                              synchronous networks
  * DKrivine/Simulation.agda: Definition of simulation relation between
                              Krivine and DKrivine configs, HeapUpdate lemmas,
                              the simulation proof itself
  * DKrivine/Soundness.agda: Corollary of Simulation: DKrivine terminates
                             with nat/diverges whenever Krivine does

The formalisation has been checked with the Agda darcs
version from Mon Feb 17 15:15:17 GMT 2014 and the Agda
standard libary from Thu Nov 28 14:29:55 GMT 2013. For
downloading instructions, see:

Other versions may also work.

Proof-of-concept compiler
See the implementation directory.