Interactive Verification of Call-by-Value Functional Programs Through a Deep Embedding

This work is now subsumed by characteristic formulae, which are implemented by the CFML tool.

The developments in the deep embedding are nevertheless accessible through the links below. Note that *_ml.v files are generated files.

Library	DeepSyntax.v DeepPrinter.v DeepSemantics.v DeepReasoning.v DeepTactics.v DeepBuiltin.v Deep.v
Verification of Caml's list library	VerifList.ml VerifList_ml.v VerifList_proof.v
Verification of a lambda-term evaluator	VerifEval.ml VerifEval_ml.v VerifEval_proof.v
Verification of a virtual machine for mini-ML	VerifByte.ml VerifByte_ml.v VerifByte_proof.v