Types for Programs and Proofs
DAT140/DIT232, study period 1, 2012"Types are the leaven of programming; they make it digestible"
(R. Milner, winner of the Turing award 1991)
NewsThe take home exam is now corrected and reported.
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 6 Sep||1-2||Introduction. Dependently typed programming. (PD) Code: TruthValues, NaturalNumbers, LambdaNotation, Lists||Homework due 20 Sep 13.15||Mo 10 Sep||3-4||Untyped Arithmetic expressions. Dependently typed programming. (PD) Code: Product, Vectors, PropositionalLogic.||Th 13 Sep||Agda programming session. (GM) Code: PredicateLogic, Equality||Mo 17 Sep||Dependently typed programming. (NAD) Code: Boolean-Expressions, Unit||Homework due 27 Sep 13.15||Th 20 Sep||5-10||Untyped lambda calculus. Simple types. Type soundness. (PD)||Mo 24 Sep||Dependently typed programming. (NAD) Code: Prelude, untyped lambda calculus, typed lambda calculus, well-typed terms, parametric higher order abstract syntax.||Homework due 4 Oct 13.15||Th 27 Sep||8-10||Simple types. Type soundness. (PD)||Mo 1 Oct||11-12||Records, variants, datatypes. Normalization. (PD)||Homework due 11 Oct 13.15||Th 4 Oct||23-25||Polymorphism and system F. Abstract data types and existential types. (PD) Code: local definitions, products and records, sums and variants, an abstract data type using a record||Mo 8 Oct||Student presentations. Schedule on wiki||Th 11 Oct||Student presentations. Schedule on wiki||Mo 15 Oct||Student presentations. Schedule on wiki||Th 18 Oct||Student presentations. Schedule on wiki.|
Viktor Holmqvist, firstname.lastname@example.org,
Jonatan Pålsson, email@example.com,
Thomas Bååth Sjöblom, firstname.lastname@example.org.