{-
  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