An Introduction to Programming and Proving with Dependent Types in Coq
Chlipala, Adam
Journal of Formalized Reasoning, Tome 3 (2010), / Harvested from Journal of Formalized Reasoning

Computer proof assistants vary along many dimensions. Among the mature implementations, the Coq system is distinguished by two key features. First, we have support for programming with dependent types in the tradition of type theory, based on dependent function types and inductive type families. Second, we have a domain-specific language for coding correct-by-construction proof automation. Though the Coq user community has grown quite large, neither of the aspects I highlight is widely used. In this tutorial, I aim to provide a pragmatic introduction to both, showing how they can bring significant improvements in productivity.

Publié le : 2010-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/1978
@article{1978,
     title = {An Introduction to Programming and Proving with Dependent Types in Coq},
     journal = {Journal of Formalized Reasoning},
     volume = {3},
     year = {2010},
     doi = {10.6092/issn.1972-5787/1978},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/1978}
}
Chlipala, Adam. An Introduction to Programming and Proving with Dependent Types in Coq. Journal of Formalized Reasoning, Tome 3 (2010) . doi : 10.6092/issn.1972-5787/1978. http://gdmltest.u-ga.fr/item/1978/