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.

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).