On this webpage we will announce the dates and agenda for future meetings and collect links to relevant resources. Contact Karl with suggested changes.
Fifth meeting is scheduled at 13:15 Tuesday 23th of June, in the Nada library. Tasks:
Fourth meeting is scheduled at 13:00 Tuesday 9th of June, in the Nada library. Tasks:
Agenda:
Third meeting is scheduled 19 March at 10:00. Room: "New York" in the main library building.
Second meeting is preliminary set to 13 March at 10:00. We have booked the Nada-library this time.
apply, intros and assumption completeness), which we completed during the meeting.
First meeting is preliminary set to 5 March at 10:00. We will talk about:
Preliminary outline of topics:
| Week | Date | Time | Location | Topics | Chapters |
|---|---|---|---|---|---|
| 10 | 2009-03-05 | 10:00 | 1635 | Introduction to Coq and demonstration of interfaces | 1.1-1.7 |
| 11 | Types, expressions, propositions and proofs | 2-3 | |||
| 12 | Dependent products and everyday logic | 4-5 | |||
| 13 | Inductive data types | 6 | |||
| 14 | Tactics, automation and inductive predicates | 7-8, 16 | |||
| 15 | Specifying functions and the module system | 9,12 | |||
| 16 | Infinite objects and proofs | 13 | |||
| 17 | Foundations of inductive types and general recursion | 14-15 |
Main text for the course is Interactive Theorem Proving and Program Development by Bertot and Casteran. We will use Coq version 8.2 with the ProofGeneral interface. All examples and exercises in the book are available as a single archive, updated for version 8.2.
Every week we will assign some exercises from the main text or the additional exercises on the web as homework to be presented the next week. These are the exercises and weeks they are due:
| Meeting | Links to solutions |
|---|---|
| 1 | Examples of two basic proofs |
| 2 | 2.1 2.2 2.3 2.4 2.5 2.6 2.7 3.2 |
| 3 | 4.1 4.2 4.2 4.5 5.1 5.2 5.3 5.4 5.5 5.6 5.7 5.8 5.9 |
| 4 | 6.1 6.2 6.3 6.4 6.5 6.6 6.7 6.8 6.9 6.17 6.18 6.23 6.30 6.31 6.32 |
| 4 | 8.1 8.5 8.6 8.7 8.9 8.10 |