Compile the examples via in-logic evaluation to Silver machine code.
helloCompileScript.sml: Compiles the hello example by evaluation inside the logic of HOL
proofs: Prove end-to-end correctness theorems for the examples as compiled to Silver machine code.
sortCompileScript.sml: Compiles the sort example by evaluation inside the logic of HOL
wordcountCompileScript.sml: Compile the wordcount program to machine code by evaluation of the compiler in the logic.