# Bachelor Seminar: Basics of Theorem Proving Using Coq

Instructor: Jannis Limperg

## Content

In this seminar, you’ll learn how to prove mathematical statements in the theorem prover Coq. In Coq, both statements and proofs can be written in a kind of functional programming language (technically: a dependent type theory). Coq then checks, according to precise rules, whether your proofs really prove your statements. Thus, if Coq accepts your proof, you can be very sure that it is, in fact, correct.

Coq can be used to prove arbitrary mathematical statements. In this seminar, we’ll look at examples from two areas of computer science:

- Algorithms and data structures: Does the program I’ve written compute the right answer? Is my implementation of a data structure correct?
- Programming language design: Does the type system of my programming language make sense? When I evaluate a program, can its type change mid-way through? Does my programming language allow me to write nonterminating programs?

## Prerequisites

- You need to be familiar with basic logic (propositional and first-order) and with basic proof techniques such as induction, proof by contradiction, etc.
- It helps if you’ve used a functional programming language (Haskell, Scala, OCaml, …) before. However, people with mathematical experience tend to find functional programming quite intuitive anyway, so this is not a hard requirement. If you’re completely new to functional programming, you may want to go through the first six chapters of the online tutorial Learn You a Haskell for Great Good before the start of the seminar. (The tutorial is for Haskell, but almost all the information there also applies to Coq.)

## Organisation

The seminar follows the free online textbook Software Foundations by Benjamin Pierce et al. It covers the whole semester and is divided into two parts:

- First, we take 7 weeks to go through the first 7 chapters of Software Foundations Vol. 1 (Logical Foundations). These teach the basics of how to write programs in Coq, how to write statements about these programs and how to prove them. You’ll study these chapters mostly on your own, but we’ll have bi-weekly meetings to discuss any questions and do some exercises.
- Second, each student chooses one of the later chapters from Software Foundations (Vol. 1-3: Logical Foundations, Programming Language Foundations, Verified Functional Algorithms) and prepares a written summary of this chapter as well as a talk. The talks are given to the whole group at the end of the semester.

I’ll also give some lectures on scientific writing and presenting.

## Examination

You’ll be graded on two products:

- A written summary of your chapter (60% of the grade). The summary must be between 7000 and 14000 characters (~3-5 pages) long.
- A talk (40% of the grade) of 20 minutes plus 5-10 minutes discussion. The talk should give an overview of the chapter.

Attendance is mandatory at the first meeting and on the presentation day(s). Attendance at the other meetings is optional but highly recommended.

## Preparation for First Meeting

To be announced.

## Chat

To be announced.

## Schedule

To be announced.

Artikelaktionen