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.

catProgScript.sml: cat program example: concatenate and print lines from files.

compilation: Compilation of the CakeML examples to different architectures.

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.

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

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