module README where -- * Roadmap of main definitions and theorems: -- Source language. open import Lambda -- Definition of the Krivine machine constituents and transition relation. open import Krivine -- Krivine is deterministic. Termination and divergence. open import Krivine.Properties -- Synchronous and asynchronous networks. open import Network -- Definition of the Distributed Krivine machine constituents and transition relation. open import DKrivine -- Point-to-point, determinism, conversion between asynchronous and synchronous networks, -- termination and divergence for networks. open import DKrivine.Properties -- Simulation relation between Krivine and DKrivine configs, HeapUpdate lemmas open import DKrivine.Simulation -- Corollary of simulation: DKrivine terminates/diverges whenever Krivine does open import DKrivine.Soundness