# Proofs and reliable programming using Coq

This is a course in 4 modules of 3 hours each, with the following tentative plan

1. Programming with simple types and recursive data-types
2. Logical formulas and the proposition-as-type correspondence in practice
3. Tactic-based theorem proving
4. Reasoning by induction on programs

Course notes: lesson 1, lesson 2, lessons 3-4, lesson 5, lesson 6, lesson 7

Useful links: a short tutorial Coq in a Hurry, a book Mathematical Components, another book for american graduate students Software Foundations, an in-browser Coq instantiation, the Coq website, and the Coq installation page.

### 1. Programming with simple types and recursive data-types

In this lesson we learn the basics of pattern-matching and recursive programming in the Coq system, using first the list data structure and then the natural number data structure as examples. This is also the occasion to teach about notations and implicit arguments. These notes cover the main part of this lesson. To test whether you understood this lesson, here are a few diagnostic questions and the corresponding answers. Please contact the teacher if these diagnostic questions show there is still some misconceptions.

### 2. Logical formulas and the proposition-as-type correspondence in practice

In this lesson, we practice the syntax of a variety of logical connectives. These notes cover the main part of this lesson. The table in this quick reference page summarizes the tactics that were taught. Diagnostic questions, answers.

### 3. Reasoning by cases and by induction about programs and their behavior

In this lesson, we show how reasoning about programs can be organized. These notes cover the main part of the lesson, diagnostic questions, answers.

### 4. Reasoning by induction, continued

In this less we continue the presentation of tactics that are useful to reason about programs. We work on a few exercises taken from the previous lesson’s notes. Homework is based on question 5(a) from these notes.