Lab Course: The Coq Proof Assistant
| Supervision | Prof. Dr. Peter Thiemann |
| Time and Place | Thu 14:00 -- 16:00, Geb 79 SR 00-019 |
| Assistance | Luminous Fennell |
Kick-Off Meeting
Thu 2015-04-30, 14:00 -- 16:00, Geb 79 SR 00-019. The room is upstairs, on the left hand side.
Infos
Dates
| Thu 2015-04-30 | Kick-off meeting |
Timetable (preliminary)
Please see the SF Roadmap for the order in which to read the chapters. We will follow the blue path.
| Date | Meeting | Chapters Read Until | Graded Exercises |
| (-> distribution) | |||
| (<- deadline) | |||
| 2015-04-30 | yes | ||
| 2015-05-07 | yes | -> ex1 | |
| 2015-05-21 | yes | Poly | -> ex2 |
| 2015-05-28 | no | <- ex1 | |
| 2015-06-11 | yes | MoreLogic | -> ex3 |
| 2015-06-20 | no | <- ex2 | |
| 2015-06-25 | yes | Hoare2 | |
| 2015-07-12 | no | <- ex3 | |
| 2015-07-09 | yes | Types | |
| 2015-07-16 | no | -> ex4 | |
| 2015-07-23 | yes | STLC, Typechecking | |
| 2015-08-06 | no | <- ex4 |
Description
The purpose of this lab course is to introduce the participants to interactive theorem proving with the Coq proof assistant. The participants will work on selected chapters from the self-study course Software Foundations of Benjamin Pierce et al. There will be periodical lab-sessions where questions, exercises and specific topics will be discussed in detail.
Covered Topics
- Basic acquaintance with the Coq proof assistant and its underlying theory
- Stating and proving formal mathematical theorems in Coq
- Proof automation/proof search
- Formalization of simple programming languages (i.e. precise definition of their behavior and proofs of their important properties)
Examination
There will be four graded exercises throughout the semester, each of which counts 25% for the final grade. In order to pass the lab course, a final grade of 4.0 or better is required.
Requirements
No specific previous knowledge of the topic is required, as the course introduces all necessary concepts. However, participants should have taken some basic logic (or logic-related) course in the past, and should have some interest in logic, formal methods, programming languages, or related topics.
The required software should be installable on all major operating systems.