cakeml/examples at master · harpreetbhatia/cakeml · GitHub

Name		Name	Last commit message	Last commit date
parent directory ..
compilation		compilation
Holmakefile		Holmakefile
README.md		README.md
catProgScript.sml		catProgScript.sml
diffProgScript.sml		diffProgScript.sml
diffScript.sml		diffScript.sml
echoProgScript.sml		echoProgScript.sml
grepProgScript.sml		grepProgScript.sml
helloErrProgScript.sml		helloErrProgScript.sml
helloProgScript.sml		helloProgScript.sml
insertSortProgScript.sml		insertSortProgScript.sml
iocatProgScript.sml		iocatProgScript.sml
lcsScript.sml		lcsScript.sml
patchProgScript.sml		patchProgScript.sml
queueProgScript.sml		queueProgScript.sml
quicksortProgScript.sml		quicksortProgScript.sml
readmePrefix		readmePrefix
sortProgScript.sml		sortProgScript.sml
splitwordsScript.sml		splitwordsScript.sml
stackProgScript.sml		stackProgScript.sml
wordcountProgScript.sml		wordcountProgScript.sml

README.md

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.

compilation: Theories for compiling the examples in the logic