An Introduction to Programming and Proving with Dependent Types in Coq

Adam Chlipala


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.

Full Text:

PDF (English)

DOI: 10.6092/issn.1972-5787/1978

Copyright (c) 2010 Adam Chlipala

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.