Compile the examples via in-logic evaluation to x86 machine code.
catCompileScript.sml: Compiles the cat example by evaluation inside the logic of HOL
diffCompileScript.sml: Compiles the diff example by evaluation inside the logic of HOL
echoCompileScript.sml: Compiles the echo example by evaluation inside the logic of HOL
grepCompileScript.sml: Compiles the grep example by evaluation inside the logic of HOL
helloCompileScript.sml: Compiles the hello example by evaluation inside the logic of HOL
helloErrCompileScript.sml: Compiles the helloErr example by evaluation inside the logic of HOL
iocatCompileScript.sml: Compiles the iocat example by evaluation inside the logic of HOL
patchCompileScript.sml: Compiles the patch example by evaluation inside the logic of HOL
proofs: Prove end-to-end correctness theorems for the examples as compiled to x86 machine code.
sortCompileScript.sml: Compiles the sort example by evaluation inside the logic of HOL
test_interpreterScript.sml: Test insertion of interpreter
wordcountCompileScript.sml: Compile the wordcount program to machine code by evaluation of the compiler in the logic.