Types for Programs and Proofs
DAT140/DIT232, study period 1, 2013
NewsThe 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 type-based 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||1-2||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 Curry-Howard isomorphism. (PD) Code: Propositional logic. Predicate logic, Equality||Mo 16 Sep||3-4||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||5-10||Dependently typed programming. (UN) Code: Proofs about Boolean expressions.||Mo 23 Sep||8-10||Untyped lambda calculus, Simple types. Type soundness. (TC)||Th 26 Sep||8-10||Simple types. Type soundness. (TC) Here is a description of simply typed lambda-calculus using de Bruijn notations and the notion of closures.||Homework due 10 Oct 13.15||Mo 30 Sep||11-12||Polymorphism and system F. Abstract data types and existential types. Normalization. (TC)||Th 3 Oct||23-25||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).