T12: An Introduction to the Coq Proof Assistant

Abstract

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.

Tutorial objectives

By the end of the tutorial, participants should be able to

1) write simple functional programs in Coq, 2) write precise program specifications, and 3) connect 1 and 2 via formal proofs.

Target audience

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

Participants will be expected to have a working installation of Coq 8.4 on their laptops along with a working IDE. (See here). They should also download the newest version of the Software Foundations textbook, which we will use to introduce Coq.

Robert Rand and Arthur Azevedo de Amorim

Robert and Arthur are PhD candidates at the University of Pennsylvania. Arthur is a collaborator on the Software Foundations textbook.