| Th 1 Sep (PD) |
Introduction.
Simply typed programming in Agda.
Code:
Booleans,
Natural numbers.
Reading: DTW 1, 2.1 - 2.5.
| Mo 5 Sep (PD) |
Termination checking. Dependent types. Polymorphism. Propositions as sets.
Code:
Division,
Logical Framework,
Lists,
Pairs,
Vectors,
Propositional logic.
Identity set,
Proofs about booleans.
DTW 2.6 - 2.7, 3, 4.1, 4.3, 5.1, 5.2.
| Th 8 Sep (PD) |
Predicate logic. Proving in Agda.
Code:
Predicate logic,
Proofs about natural
numbers. DTW 4.2, 4.4.
| Mo 12 Sep (PD) |
Inductive Predicates. Records. Abstract data types.
Code:
Even numbers,
A record for dates,
Products as records,
The Sigma-type as a dependent record,
Counters as records.
Homework 1 due.
| Th 15 Sep (TC) |
Introduction to operational semantics and type systems.
| Mo 19 Sep (TC) |
Introduction to operational semantics and type
systems. Homework 2 due.
| Th 22 Sep (PD) |
Boolean expressions and
arithmetic expressions in Agda.
Code:
Boolean expressions,
Operational semantics of
Boolean expressions,
Reflexive, transitive
closure of a relation,
Arithmetic expressions and their types,
Operational semantics of
artihmetic expressions and the proof of the type preservation theorem.
| Mo 26 Sep (TC) |
Introduction to operational semantics and type
systems. Homework 3 due.
| Th 29 Sep (TC) |
Introduction to operational semantics and type systems.
| Mo 3 Oct (TC) |
Introduction to operational semantics and type systems.
| Th 6 Oct (UN) |
Guest lecture on Agda.
Code:
Typed lambda calculus.
| Mo 10 Oct |
Student presentations.
Homework 4 due.
| Th 13 Oct |
Student presentations.
| Mo 17 Oct |
Student presentations.
|
