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

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.

proofs: Correctness proof for the CakeML compiler.