Types for Programs and ProofsDAT140/DIT232, study period 1, 2013NewsThe take home exam is now corrected. Unfortunately, we have not been able to do the official reporting of the course because of illness at the student administration office.AimThe development of powerful type systems is one of the most dynamic aspects of modern programming language design. The aim of this course is to provide a solid and broad foundation in type systems for programming languages. The student will be exposed to applications of typebased technology in computer science and learn to use an interactive programming and proof system using dependent types.LiteratureTypes and Programming Languages by Benjamin Pierce, MIT Press.

Date  Chapters  Topics  Homework 
Th 5 Sep  12  Introduction. Dependently typed programming in Agda. (PD)  Homework due 19 Sep 13.15 
Mo 9 Sep  Dependently typed programming in Agda. (PD) Code: Truth values, Natural numbers, Lambda notation, Lists, Pairs, Unit, Vectors.  
Th 12 Sep  The CurryHoward isomorphism. (PD) Code: Propositional logic. Predicate logic, Equality  
Mo 16 Sep  34  Proving in Agda. Boolean expressions and untyped lambda expressions in Agda (PD) Code: Proofs about booleans, Proofs about natural numbers, Boolean expressions, Untyped lambda expressions  Homework due 26 Sep 13.15 
Th 19 Sep  510  Dependently typed programming. (UN) Code: Proofs about Boolean expressions.  
Mo 23 Sep  810  Untyped lambda calculus, Simple types. Type soundness. (TC)  
Th 26 Sep  810  Simple types. Type soundness. (TC) Here is a description of simply typed lambdacalculus using de Bruijn notations and the notion of closures.  Homework due 10 Oct 13.15 
Mo 30 Sep  1112  Polymorphism and system F. Abstract data types and existential types. Normalization. (TC)  
Th 3 Oct  2325  Introduction to univalent foundations. (TC)  
Mo 7 Oct  Student presentations. Schedule on wiki  
Th 10 Oct  Student presentations. Schedule on wiki  
Mo 14 Oct  Student presentations. Schedule on wiki  
Th 17 Oct  Student presentations. Schedule on wiki. 
Bonus points will also be given for good presentations (max 5 pts) and for attendance at the presentations (max 4 x 1 pts).