A verified compiler for CakeML, including:
- lexing and PEG parsing,
- type inference,
- compilation to ASM assembly language, and,
- code generation to x86, ARM, and more.
backend: The CakeML compiler backend.
benchmarks: Two benchmark suites for the CakeML compiler.
bootstrap: Theories that perform proof-grounded bootstrapping of the CakeML compiler in HOL.
compilationLib.sml: Library for in-logic compilation of CakeML abstract syntax producing machine code (for a variety of targets) using the CakeML compiler backend.
compilerScript.sml: Definition of the CakeML compiler as a function that takes a list of command line arguments and a string corresponding to standard input, and produces a pair of output strings for standard error and standard output (the latter containing the generated machine code if successful).
dafny: Translate Dafny into CakeML.
encoders: Encoders for CakeML's ASM abstract assembly language into each of the concrete targets of the CakeML compiler.
inference: The CakeML type inferencer.
parsing: The CakeML parser.
printing: The printer mechanism for the CakeML REPL.
proofs: Correctness proof for the CakeML compiler.
repl: Some definitions and proofs used in the proof of the CakeML and Candle read-eval-print loop (REPL).