I
Icing
A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.
-
Heiko Becker authoredf63a86a5
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... |