POPL 2016:
Programs and Proofs in the Coq Proof Assistant

By Arthur Azevedo de Amorim and Robert Rand
University of Pennsylvania

Materials

• 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

Introduction

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).

Further Reading

• 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