| Date |
Chapters |
Topics |
Homework |
Th 4 Sep |
1-3 |
Introduction. Arithmetic expressions (TC)
| Homework due 15 Sep 13.15
| Mo 8 Sep |
|
Haskell-like programming in Agda. (PD)
Code:
Booleans,
Natural numbers,
Lambda notation,
| Th 11 Sep |
|
Dependent types. Propositions as sets. (PD)
Code:
Lists,
Pairs,
Vectors,
Propositional logic.
| Homework due 22 Sep 13.15
| Mo 15 Sep |
|
Predicate logic. Proving in Agda (PD)
Code: Predicate logic,
Identity,
Proofs about booleans,
Proofs about natural
numbers.
| Th 18 Sep |
3-4 |
Proving in Agda. Boolean expressions and untyped
lambda expressions in Agda (PD)
Code:
Boolean expressions,
Products as records,
Counters as records,
Finite sets,
Untyped lambda expressions
Typed lambda expressions
| Homework due 29 Sep 13.15
| Mo 22 Sep |
|
Dependently typed programming. (UN)
Code: An evaluator for typed lambda terms.
| Th 25 Sep |
5-10 |
Simply typed lambda calculus. Type soundness. (TC) Description of
simply typed lambda-calculus with de Bruijn
notations and closures.
| Homework due 6 Oct 13.15
| Mo 29 Sep |
11-12 |
Polymorphism and system F. Abstract data types and
existential types. Normalization. (TC)
|
Th 2 Oct |
23-25 |
Introduction to univalent foundations. (TC)
| Mo 6 Oct |
| Student presentations.
| Th 9 Oct |
| Student presentations.
| Mo 13 Oct |
| Student presentations.
| Th 16 Oct |
| Student presentations.
| Mo 20 Oct |
| Student presentations.
|
