{- Formalisation of the distributed abstract machines CES, CESH and DCESH ====================================================================== Author: Olle Fredriksson Date: 2014 Compatibility: Known to work with * Agda 2.4.0.1 from hackage (https://hackage.haskell.org/package/Agda) * Agda standard library version 0.8 (http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary) Other versions may also work. -} module README where -- * Some general lemmas and imports import GeneralLemmas import Relation import Trace -- * Source language and bytecode import Lambda import MachineCode -- * The CES machine import CES import CES.Properties -- * Heap interface import Heap -- * The CESH machine import CESH import CESH.Properties -- | CES ~ CESH proof import CESH.Simulation import CESH.Presimulation import CESH.Bisimulation -- * Networks import Tagged import Network -- * The DCESH_1 machine import DCESH1 -- * The DCESH machine import DCESH import DCESH.Properties -- | CESH ~ DCESH proof import DCESH.Simulation-CESH import DCESH.Presimulation-CESH import DCESH.Bisimulation-CESH -- * Fault-tolerance import Backup