POPL 2016:
Programs and Proofs in the Coq Proof Assistant

By Arthur Azevedo de Amorim and Robert Rand
University of Pennsylvania

Materials

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

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