------------------------------------------------------------------------ -- Code related to the paper -- "Operational Semantics Using the Partiality Monad" -- -- Nils Anders Danielsson ------------------------------------------------------------------------ -- Several definitions and proofs in this code are closely related to -- definitions and proofs in the paper "Coinductive big-step -- operational semantics" by Leroy and Grall. See my paper for more -- detailed references to related work, and also for more explanations -- of how the code works. module Operational-semantics-using-the-partiality-monad where ------------------------------------------------------------------------ -- Section 2 -- Fin. import Data.Fin -- Vec, lookup. import Data.Vec -- The partiality monad. import Category.Monad.Partiality -- A variant of trivial, as well as proofs showing that the definition -- of weak bisimilarity in the paper coincides with Capretta's -- definition and a more standard definition based on weak -- bisimulations. import AdmissibleButNotPostulable ------------------------------------------------------------------------ -- Section 3 -- Tm, Env, Value. import Lambda.Syntax -- Big-step functional semantics, Ω. import Lambda.Closure.Functional -- The module above uses some workarounds in order to convince Agda -- that the code is productive. The following module contains (more or -- less) the same code without the workarounds, but is checked with -- the termination checker turned off. import Lambda.Closure.Functional.No-workarounds -- An alternative definition of the functional semantics. This -- definition uses continuation-passing style instead of bind. import Lambda.Closure.Functional.Alternative ------------------------------------------------------------------------ -- Section 4 -- Type system. import Lambda.Syntax -- Type soundness. import Lambda.Closure.Functional.Type-soundness -- The use of Lift in the paper is replaced by the use of two -- different predicate transformers: Any for Maybe and All for the -- partiality monad. import Data.Maybe import Category.Monad.Partiality.All -- An alternative definition of the functional semantics, using -- substitutions instead of environments and closures, plus a proof of -- type soundness. import Lambda.Substitution.Functional ------------------------------------------------------------------------ -- Section 5 -- The relational semantics. import Lambda.Closure.Relational -- Proofs of equivalence. import Lambda.Closure.Equivalence ------------------------------------------------------------------------ -- Section 6 -- The virtual machine. Two semantics are given, one relational and -- one functional, and they are proved to be equivalent. import Lambda.VirtualMachine ------------------------------------------------------------------------ -- Section 7 -- The compiler. import Lambda.VirtualMachine -- Compiler correctness for the functional semantics. import Lambda.Closure.Functional import Lambda.Closure.Functional.No-workarounds -- Compiler correctness for the relational semantics. import Lambda.Closure.Relational ------------------------------------------------------------------------ -- Section 8 -- The non-deterministic language along with a compiler and a compiler -- correctness proof, as well as a type soundness proof. import Lambda.Closure.Functional.Non-deterministic import Lambda.Closure.Functional.Non-deterministic.No-workarounds ------------------------------------------------------------------------ -- Section 9 -- A very brief treatment of different kinds of term equivalences, -- including contextual equivalence and applicative bisimilarity. import Lambda.Closure.Equivalences -- _⇓. import Category.Monad.Partiality