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