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...