Reference. One Step at a Time: A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts
Cite
Cites 28 works (1 here)
With notes (1)
CakeML: A verified implementation of ML kumar_cakeml_2014
We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitraryprecision arithmetic, and compiler bootstrapping.
External (27)
- Collapsing towers of interpreters (2017)
- Deriving pretty-big-step semantics from small-step semantics (2014)
- From small-step semantics to big-step semantics, automatically (2013)
- Engineering definitional interpreters (2013)
- Pretty-Big-Step Semantics (2013)
- An executable formal semantics of C with applications (2012)
- A walk in the semantic park (2011)
- A small step for mankind (2010)
- An overview of the K semantic framework (2010)
- Semantics Engineering with PLT Redex (2009)
- Coinductive big-step operational semantics (2009)
- Defunctionalized interpreters for programming languages (2008)
- A machine-checked model for a Java-like language, virtual machine, and compiler (2006)
- From natural semantics to abstract machines (2005)
- From Reduction-based to Reduction-free Normalization (2005)
- Refocusing in Reduction Semantics (2004)
- On evaluation contexts, continuations, and the rest of computation (2004)
- Specification and correctness of lambda lifting (2003)
- A Selective CPS Transformation (2001)
- Continuations: A Mathematical Semantics for Handling Full Jumps (2000)
- Definitional Interpreters for Higher-Order Programming Languages (1998)
- The Definition of Standard ML (1997)
- A Syntactic Approach to Type Soundness (1994)
- Representing Control: a Study of the CPS Transformation (1992)
- An operational semantics for CSP (Oxford tech report) (1986)
- Communicating Sequential Processes (1985)
- Lambda lifting: transforming programs to recursive equations (1985)