Reference. One Step at a Time: A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts

Cite

Cite as @vesely-2019-one (helia, typst) · \cite{vesely-2019-one} (LaTeX)
BibTeX
bibtex · 1 line
@inbook{vesely-2019-one, title={One Step at a Time: A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts}, ISBN={9783030171841}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-030-17184-1_8}, DOI={10.1007/978-3-030-17184-1_8}, booktitle={Programming Languages and Systems}, publisher={Springer International Publishing}, author={Vesely, Ferdinand and Fisher, Kathleen}, year={2019}, pages={205–231} }
hayagriva YAML (typst)
yaml · 17 lines
vesely-2019-one:
  type: chapter
  title: 'One Step at a Time: A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts'
  author:
  - Vesely, Ferdinand
  - Fisher, Kathleen
  date: 2019
  page-range: 205-231
  url: http://dx.doi.org/10.1007/978-3-030-17184-1_8
  serial-number:
    doi: 10.1007/978-3-030-17184-1_8
    isbn: '9783030171841'
    issn: 1611-3349
  parent:
    type: book
    title: Programming Languages and Systems
    publisher: Springer International Publishing
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.
PDF · DOI · pldb
vesely-2019-one reference entries/refs/vesely-2019-one/vesely-2019-one.hel