This directory contains solutions for the tutorial.

simple_bstScript.sml: Simple binary search tree.

splitwordsScript.sml: A high-level specification of words and frequencies

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.