FONTAINE , Arnaud

Coq is a formal system which provides both a pure, functional programminglanguage with dependent types, and an environment to write machine-checkedproofs.Using Coq, it is possible to model a system, to formalize properties this systemis expected to satisfy, and to prove the correctness of the model with respectto these properties.Coq has...