HTTPS clone URL
Subversion checkout URL
CakeML: A Verified Implementation of ML
Standard ML Haskell OCaml Shell PHP Assembly
The CakeML project (https://cakeml.org). A verified implementation of a significant subset of Standard ML in the HOL4 theorem prover (http://hol-theorem-prover.org). We build CakeML using the latest development version of HOL4. We build HOL on PolyML 5.5.2 (http://www.polyml.org). This branch (master) contains the latest development version of CakeML. See the version1 branch for the previous version. Directory structure: - semantics The definition of CakeML, including - its concrete syntax - its abstract syntax - small step semantics - big step semantics (both functional and relational) - semantics of FFI calls - a type system The definition is (mostly) expressed in Lem (http://www.cs.kent.ac.uk/~sao/lem), but the generated HOL is also included. - semantics/proofs Metatheory of CakeML and other proofs about the semantics - a verified, clocked interpreter - determinism - type soundness - equivalence of the big and small step semantics - equivalence of functional and relational semantics - compiler A verified compiler for CakeML, including: - parsing: lexer and PEG parser - inference: type inferencer - backend: compilation to ASM assembly language - targets: code generation to x86, ARM, and more - translator A proof-producing translator from HOL functions to CakeML. - unverified/interp Unverified implementation, in Haskell, of the CakeML frontend augmented with informative error messages. - unverified/bytecode An unverified implementation of CakeML bytecode, written in C - candle Verification of a HOL theorem prover, based on HOL Light (http://www.cl.cam.ac.uk/~jrh13/hol-light/), implemented in CakeML. - explorer Tools for stepping through execution of the compiler from one intermediate language to the next, and pretty-printing the intermediate results. An instance is available on the CakeML website. - mlstringScript.sml, mlstringLib.sml, mlstringSyntax.sml Small theory of wrapped strings, so the translator can distinguish them from char lists and target CakeML strings. - compute_basicLib.sml Build compsets for evaluation in the logic. - miscLib.sml, miscScript.sml, preamble.sml Theorems and proof tools (e.g. tactics) used throughout the development. - lem_lib_stub empty versions of the Lem libraries (which we don't use, but building with Lem requires) - developers scripts for running regression tests and other miscellany - COPYING Copyright notice, license, and disclaimer.