An Introduction to the Coq Proof Assistant
By Arthur Azevedo de Amorim and Robert Rand
University of Pennsylvania
- Coq 8.4
- Proof General (recommended for emacs users)
- Tutorial: Programs and Proofs [with holes, without holes]
- Tutorial: Red-Black Trees [with holes, without holes]
- Tactics Cheat Sheet
This tutorial will focus on functional programming and mathematical proofs using the Coq proof assistant. Coq is a dependently typed functional programming language that can be used to write programs and verify that they meet a variety of given specifications. This allows to develop software that is correct by construction, in which a variety of possible bugs and exceptions are ruled out a priori.By the end of the tutorial, participants should be able to
- Write simple functional programs in Coq
- Write precise program specifications
- Connect 1 and 2 via formal proofs.
This tutorial is aimed at programmers with some knowledge of functional programming who are interested in writing highly reliable programs in Coq or a related language (such as Haskell, Agda or Isabelle).