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

Before the first meeting on 18th Oct 2023, please clone this Git repository and follow the installation instructions in the README. We can fix any problems during the meeting, but if everyone only discovers these problems then and there, we won’t get anywhere.

Chat

There’s a chatroom for this seminar on the IFI Zulip chat:

Server: https://chat.ifi.lmu.de Stream: TCS-23W-Coq

Please use this chat to discuss questions about the seminar, whether about the organisation or the content. This is much more efficient than sending me emails because everyone can immediately see the questions and answers.

Schedule

We meet periodically on Wednesdays (with exceptions) from 14:15 to 15:45 (both s.t.) at Oettingenstraße 67, room L109. See below for the exact dates and topics.