kumar_cakeml_2014:
  type: article
  title:
    value: '{CakeML}: a verified implementation of {ML}'
    short: '{CakeML}'
  author:
  - Kumar, Ramana
  - Myreen, Magnus O.
  - Norrish, Michael
  - Owens, Scott
  date: 2014-01
  page-range: 179-191
  url:
    value: https://dl.acm.org/doi/10.1145/2535838.2535841
    date: 2024-04-22
  serial-number:
    doi: 10.1145/2535838.2535841
    isbn: 978-1-4503-2544-8
  abstract: 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.
  parent:
    type: proceedings
    title: Proceedings of the 41st {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}
    publisher:
      name: ACM
      location: San Diego California USA