Definition of Dafny's semantics.
dafny_compilerProofScript.sml: Correctness proof for the Dafny to CakeML compiler.
dafny_evaluateScript.sml: Functional big-step semantics for evaluation of Dafny programs.
dafny_semanticPrimitivesScript.sml: Definition of semantic primitives used in the semantics.