Programs and Proofs in the Coq Proof Assistant
By Arthur Azevedo de Amorim and Robert Rand
University of Pennsylvania
- Coq 8.4
- Proof General (recommended for emacs users)
- Session 1: Programs and Proofs [short, full, solutions]
- Session 2: Data Structures and Automation [short, full, solutions]
- Extra Material: Arithmetic
- Git Repository
- 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).
- The Official Coq Documentation
- Software Foundations - a thorough introduction to Coq, logic and type theory.
- Certified Programming with Dependent Types - a guide to certified Coq programming.
- Benjamin Pierce's Coq tutorial (video)
- The Cocorico Coq Wiki
- Poleiro - the Coq blog
- The Gagallium Blog
- The CompCert Verified C Compiler
- The DeepSpec Project