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 Sigmatype 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.
