-
Everyone presents at least one topic and prepares exercises for it.
-
If you want to present some topic, write your name in the presenter column!
-
You are encouraged to pick topics that you find of interest, even if they are not currently in the syllabus.
-
If the topic is new, add your name and the title to the end of the table. We can agree on a date and make space for your presentation during the next session.
-
You can find many suggestions for topics in suggestions.md.
-
| Date | Topic | Presenter |
|---|---|---|
| 2/02 | Organization | - |
| 16/02 | "Inductively Defined Propositions" | Victor |
| 2/03 | The CoC, Prop vs Set, proof terms | Simon R. |
| 16/03 | CPDT vs. SF and infinite data & related | Andreas |
| 6/04 | No presentation: Exercises from "Types Systems" | - |
| 12/04 | AutoSubst Coq library | Andrea |
| 27/04 | Basic Ltac programming | Fabian |
| 11/05 | Proof by reflection / ssreflect | Daniel |
An overall goal is to get to "Normalization of STλC", but, depending on the topics that presenters pick and timing constraints, we might stop somewhere along the way. This will require going through the "STλC" and perhaps "STλCProp".
Presenters are not discouraged from picking other, unrelated topics. Once they have chosen a topic, they are encouraged to give examples or exercises related to the overall goal, if possible.