Arthur Charguéraud
Publications
by date
by topic
by venue
Software
CFML
TLC
PASL
FormalMetaCoq
OptiTrust
Teaching
Separation Logic
Coq tutorials
Concours Castor
France-ioi
Misc
The RE command
Home
–
Contact
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