Skip to content

Latest commit

 

History

History

examples

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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