# 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