# T12: An Introduction to the Coq Proof Assistant

- Robert Rand University of Pennsylvania
- Arthur Azevedo de Amorim University of Pennsylvania

September 04, 2015 1:30 - 5:00 PM

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