Examples of verified programs built using CakeML infrastructure.
Larger examples (like the CakeML compiler and Candle theorem prover) can be found in their own top-level directories.
array_searchProgScript.sml: An example based on searching an array.
bot: Formalization of the FFI and proofs for the VeriPhy pipeline.
catProgScript.sml: cat program example: concatenate and print lines from files.
compilation: Compilation of the CakeML examples to different architectures.
cost: Preliminary data-cost examples
deflate: Scripts relevant to the formalisation of the DEFLATE algorithm
diffProgScript.sml: diff example: find a patch representing the difference between two files.
diffScript.sml: Implementation and verification of diff and patch algorithms
divScript.sml: Examples of non-termination.
doubleArgProgScript.sml: Examples on the topic of doubling a number.
echoProgScript.sml: echo program example: print the command line arguments.
eval: A simple example of using eval, to help work out the development of the bootstrapped compiler supporting eval.
filterProgScript.sml: Filter case study from CASE.
grepProgScript.sml: grep example: search for file lines matching a regular expression.
helloErrProgScript.sml: Hello World on standard error.
helloProgScript.sml: Hello World example, printing to standard output.
insertSortProgScript.sml: In-place insertion sort on a polymorphic array.
iocatProgScript.sml: Faster cat: process 2048 chars at a time.
lcsScript.sml: Verification of longest common subsequence algorithms.
lispProgScript.sml: Parsing and pretty printing of s-expressions
lpr_checker: An LPR checker built on CakeML
md5ProgScript.sml: Translate md5 function
md5Script.sml: Functional definition of md5 hash based on HOL/src/portableML/poly/MD5.sml
opentheory: Implementation of an OpenTheory reader based on the Candle kernel.
patchProgScript.sml: patch example: apply a patch to a file.
pseudo_bool: A checker for pseudo-boolean constraints
queueProgScript.sml: An example of a queue data structure implemented using CakeML arrays, verified using CF.
quicksortProgScript.sml: In-place quick sort on a polymorphic array.
replProgScript.sml: The CakeML REPL
sat_encodings: Encodings of puzzles to CNF, to use as SAT-solver input.
sortProgScript.sml: Program to sort the lines in a file, built on top of the quick sort example.
splitwordsScript.sml: A high-level specification of words and frequencies
stackProgScript.sml: An example of a stack data structure implemented using CakeML arrays, verified using CF.
vipr: Formalisation of VIPR: Verifying Integer Programming Results https://github.com/ambros-gleixner/VIPR
wordcountProgScript.sml: Simple wordcount program, to demonstrate use of CF.
xlrup_checker: An XLRUP checker built on CakeML