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.

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

compilation: Theories for compiling the examples in the logic

diffProgScript.sml: diff example: find a patch representing the difference between two files.

diffScript.sml: Implementation and verification of diff and patch algorithms

echoProgScript.sml: echo program example: print the command line arguments.

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.

patchProgScript.sml: patch example: apply a patch to a file.

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.

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.

wordcountProgScript.sml: Simple wordcount program, to demonstrate use of CF.