Materials
You need to login in order to access more course material.
Assignments
| Assignment 1 (145 KB) | rev 1 | ||
| Assignment 2 (184 KB) | rev 5 | ||
| Assignment 3 (65 KB) | rev 6 | ||
| Assignment 4 (62 KB) | rev 2 | ||
| Assignment 5 (52 KB) | rev 4 | ||
| Assignment 6 (51 KB) | rev 5 | ||
| Assignment 7 (175 KB) | rev 6 | ||
| Assignment 8 (50 KB) | rev 3 | ||
| Assignment 9 (176 KB) | rev 2 | ||
| Assignment 10 (48 KB) | rev 1 | ||
| Assignment 11 (41 KB) | rev 1 | ||
| Assignment 12 (46 KB) | rev 2 | ||
| Assignment 13 (56 KB) | rev 1 | ||
| Assignment 14 (49 KB) | rev 1 | ||
| Coq Sources for Assignment 1 (2.0 KB) | rev 1 | ||
| Coq Sources for Assignment 2 (4.1 KB) | rev 2 | ||
| Coq Sources for Assignment 3 (4.1 KB) | rev 4 | ||
| Coq Sources for Assignment 4 (4.9 KB) | rev 1 | ||
| Coq Sources for Assignment 5 (3.3 KB) | rev 2 | ||
| Coq Sources for Assignment 6 (4.4 KB) | rev 2 | ||
| Coq Sources for Assignment 7 (4.8 KB) | rev 2 | ||
| Coq Sources for Assignment 8 (1.2 KB) | rev 1 | ||
| Coq Sources for Assignment 9 (1.2 KB) | rev 1 | ||
| Coq Sources for Assignment 12 (11 KB) | rev 1 | ||
| Coq Sources for Assignment 13 (8.2 KB) | rev 1 |
| Demo 04-20 (1.1 KB) | Booleans, numbers, inductive proofs | rev 2 | |
| Demo 04-25 (2.2 KB) | Pairs and iteration, dependent function types, implicit arguments | rev 3 | |
| Demo 04-27 (674 Bytes) | Propositions as types | rev 1 | |
| Demo 05-02 (1003 Bytes) | Existential quantification, excluded middle | rev 1 | |
| Demo 05-04 (1.7 KB) | Impredicative characterisations, propositional equality | rev 3 | |
| Demo 05-09 (2.9 KB) | Discrete types; Ackermann; primitive recursion; induction lemma. | rev 1 | |
| Demo 05-11 (3.1 KB) | Primitive recursion; Truth value semantics; Elim restriction; Hurkens paradox | rev 2 | |
| Demo 05-16 (1.5 KB) | inductive predicates, le and safe | rev 1 | |
| Demo 05-18 (2.0 KB) | inductive predicate y <= y | rev 1 | |
| Demo 05-23 (1.0 KB) | Inversion and induction lemmas | rev 1 | |
| Demo 05-30 (1.9 KB) | Lists | rev 1 | |
| Demo 06-01 (2.3 KB) | Decidability | rev 2 | |
| Demo 06-06 (3.9 KB) | Discrete types | rev 3 | |
| Demo 06-13 (2.1 KB) |
Options, sums, refinement types, find, choice functions |
rev 1 | |
| Demo 06-20 (1.6 KB) | Diaconescu's theorem and acc | rev 1 | |
| Demo 06-22 (2.5 KB) | Constructive Choice | rev 1 | |
| Demo 06-27 (3.5 KB) | Retracts | rev 3 | |
| Demo 06-29 (3.0 KB) | Inheritance of choice functions | rev 2 | |
| Demo 07-04 (5.8 KB) | Binary trees over numbers are countable | rev 1 | |
| Demo 07-06 (5.6 KB) | Normalisers, quotients, Cantor | rev 2 | |
| Demo 07-11 (1.8 KB) | Intuitionistic ND | rev 1 | |
| Demo 07-13 (3.0 KB) | Heyting entailment | rev 1 | |
| Demo 07-18 (4.4 KB) | Sandwich theorem for entailment predicates | rev 1 |
| Classical Tableau Method (64 KB) | rev 3 | ||
| Constructive Choice (73 KB) | rev 3 | ||
| Decidability (76 KB) | rev 6 | ||
| Identity Proofs (51 KB) | rev 1 | ||
| Induction and Recursion for Numbers (65 KB) | rev 1 | ||
| Inductive Predicates (91 KB) | rev 18 | ||
| Lists (66 KB) | rev 3 | ||
| Natural Deduction (85 KB) | rev 9 | ||
| Option Types and Sigma Types (77 KB) | rev 4 | ||
| Proof Irrelevance and Elim Restriction (57 KB) | rev 7 | ||
| Retracts (89 KB) | rev 17 |
A new assignment sheet will be published every week. It will neither be corrected nor graded. After one week, we will publish a sample solution that you can compare your own solutions to. If you have further questions, you can discuss them in your tutorial group, during the office hour, and on the discussion board.