------------------------------------------------------------------------ -- Imports all the other modules ------------------------------------------------------------------------ module Everything where -- The syntax of a simple language with exceptions and interrupts -- (asynchronous exceptions). import Syntax -- An abstract specification of a semantics. import Semantics -- Big-step semantics. import Semantics.BigStep -- Infinite transition sequences, used by the small-step semantics. import Infinite -- Small-step semantics. import Semantics.SmallStep import Semantics.SmallStep.EvalCtxt -- The two semantics are equivalent. import Semantics.Equivalence import Semantics.Equivalence.Lemmas -- Definition of equivalence between two expressions. Uses the -- big-step semantics. import Equivalence -- Some properties related to totality. import Totality -- Lemmas about the interrupt-block status. import StatusLemmas -- Some simple algebraic properties. import AlgebraicProperties -- A virtual machine and a compiler. import VirtualMachine -- The bar relation, used to state compiler correctness. import Bar -- Statement of compiler correctness. import CompilerCorrectness -- Proof of compiler correctness for the big-step semantics. One part -- of this proof makes use of the small-step semantics. import Semantics.BigStep.CompilerCorrectness.Completeness import Semantics.BigStep.CompilerCorrectness.BarTheorem import Semantics.BigStep.CompilerCorrectness.Soundness import Semantics.BigStep.CompilerCorrectness -- Partial proof of compiler correctness for the small-step semantics. import Semantics.SmallStep.CompilerCorrectness.Soundness