This directory contains the definition of the semantics for each intermediate language that is used in the compiler backend. This directory also contains generic properties about the semantics of each intermediate language.
backendPropsScript.sml: General definitions and theorems that are useful within the proofs about the compiler backend.
bviPropsScript.sml: Properties about BVI and its semantics
bviSemScript.sml: The formal semantics of BVI
bvlPropsScript.sml: Properties about BVL and its semantics
bvlSemScript.sml: The formal semantics of BVL
closPropsScript.sml: Properties about closLang and its semantics
closSemScript.sml: The formal semantics of closLang
dataPropsScript.sml: Properties about dataLang and its semantics
dataSemScript.sml: The formal semantics of dataLang
data_monadScript.sml: Define a monad to make dataLang ASTs nicer to work with
flatPropsScript.sml: Properties about flatLang and its semantics
flatSemScript.sml: The formal semantics of flatLang
labPropsScript.sml: Properties about labLang and its semantics
labSemScript.sml: The formal semantics of labLang
stackPropsScript.sml: Properties about stackLang and its semantics
stackSemScript.sml: The formal semantics of stackLang
targetPropsScript.sml: Properties about the target semantics
targetSemScript.sml: The formal semantics of the target machine language. This semantics is parametrised by the target configuration, which includes the next state function of the target architecture.
target_itreeEquivScript.sml:
Theorem expressing machine_sem in terms of target itree semantics
target_itreePropsScript.sml: Properties about the itree target semantics
target_itreeSemScript.sml: An itree-based semantics for the target machine code
wordPropsScript.sml: Properties about wordLang and its semantics
wordSemScript.sml: The formal semantics of wordLang