Icing

Project ID: 1140

A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.

Name	Last commit	Last update
.gitignore		Loading commit data...
CakeMLconnProofsScript.sml		Loading commit data...
CakeMLconnScript.sml		Loading commit data...
CompilerProofsScript.sml		Loading commit data...
CompilerScript.sml		Loading commit data...
CompilerTacticsLib.sml		Loading commit data...
Holmakefile		Loading commit data...
Instructions_CAV_Artifact.txt		Loading commit data...
README.md		Loading commit data...
SemanticsScript.sml		Loading commit data...
SyntaxScript.sml		Loading commit data...
exampleScript.sml		Loading commit data...
icingPreamble.sml		Loading commit data...
lexerParserScript.sml		Loading commit data...
patternProofsScript.sml		Loading commit data...
patternScript.sml		Loading commit data...
patternTacticsLib.sml		Loading commit data...
rewriteRulesProofsScript.sml		Loading commit data...
rewriteRulesScript.sml		Loading commit data...
simRelScript.sml		Loading commit data...
valueTreesScript.sml		Loading commit data...
wellDefinedExpScript.sml		Loading commit data...