The source language is defined in files:
- source_syntaxScript.sml
- source_valuesScript.sml
- source_semanticsScript.sml
- source_propertiesScript.sml
The target assembly language is defined in files:
The code generator and its verification proof:
Functions and proofs about lexing, parsing and pretty printing of source code:
Top-level compiler definition as shallow embedding:
Automation that converts shallow embeddings into deep embeddings:
In-logic evaluation of the code generator applied to the deeply embedded compiler:
A file with the top-level correctness theorems: