This directory contains the exercises for the tutorial. They are generated from the solutions with the worked parts removed, and are not expected to build until the exercises have been solved.
arith_exp_demoScript.sml: A demonstration of interaction with HOL: a simple datatype for arithmetic expressions.
simple_bstProgScript.sml: Using the CakeML translator to produce a verified deep embedding of the simple BST implementation.
simple_bstScript.sml: Simple binary search tree.
splitwordsScript.sml: A high-level specification of words and frequencies
wordcountCompileScript.sml: Compile the wordcount program to machine code by evaluation of the compiler in the logic.
wordcountProgScript.sml: Simple wordcount program, to demonstrate use of CF.
wordcountProofScript.sml: Constructs the end-to-end correctness theorem for wordcount example by composing the application-specific correctness theorem, the compiler evaluation theorem and the compiler correctness theorem.
wordfreqCompileScript.sml: Compile the wordfreq program to machine code by evaluation of the compiler in the logic.
wordfreqProgScript.sml: The CakeML program implementing the word frequency application. This is produced by a combination of translation and CF verification.
wordfreqProofScript.sml: Constructs the end-to-end correctness theorem for wordfreq example by composing the application-specific correctness theorem, the compiler evaluation theorem and the compiler correctness theorem.