Types for Programs and Proofs
DAT140/DIT232, study period 1, 2011"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. The results will soon be available.
AimThe development of ever more 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||We 31 Sep||Part 1||Introduction. Arithmetic expressions. (TC)||Homework due 19 Sep 13.15||Mo 5 Sep||Part 1||Untyped systems. Arithmetic expressions. Types and computation rules. (TC)||We 7 Sep||8,9,10||Simple types. Type soundness. (TC)||Homework due 26 Sep 13.15||Mo 12 Sep||8,9,10||Simple types. Type soundness. (TC)||We 14 Sep||11,12||Records, variants, datatypes. Normalization. (TC)||Mo 19 Sep||Dependently typed programming in Agda. (UN)||Code: html, agda||We 21 Sep||Dependently typed programming in Agda. (UN)||Code: html, agda||Homework due 5 Okt 13.15||Deadline for scheduling student presentations.||Mo 26 Sep||23,24,25||Polymorphism and system F. Abstract data types and existential types. (PD)||We 28 Sep||Dependently typed programming in Agda. (UN)||Code: html, agda||Mo 3 Oct||Student presentations.||References, chapter 13 (Christian Isaksson, Andreas Wagner)||Subtyping, chapter 15, (Jens Lidestrm, Bart van Delft)||John McCarthy, Recursive functions of symbolic expressions and their computation by machine (Jonatan Bengtsson, Albin Lindbck)||We 5 Oct||Featherweight Java, Chapter 19 (Hannes Srensson, Vijayakumar Raju)||Rod Burstall, Proving properties of programs by structural induction (Daniel Andren, Christoffer Skeppstedt)||Tim Griffin, The Formulae-as-Types Notion of Control for Curry-Howard and classical logic (Johan Grafstrm, Rodolphe Lepigre)||Types, abstraction, and parametric polymorphism (se Fahlander, Joacim Kosonen)||Mo 10 Oct||Jean-Louis Krivine, Call-by-name lambda-calculus machine (Johan Elvek, David Spngberg)||John Launchbury, A Natural Semantics for Lazy Evaluation (Qiuchi Jian, Gabriel Rizopulos)||Phil Wadler and Robby Findler, Well-typed programs cannot be blamed, (Jonas Karlsson, Mattis Jeppsson)||We 12 Oct||Exceptions, chapter 14, (Erik Flood, Joel Svensson)||Recursive types, chapter 20 (Andreas Granstrm, Daniel Mauritzson)||Peter Landin, On the Mechanical evaluation of Expressions (Ingemar dal, Alexandiar Marschanka)||John Reynolds, Towards a Theory of Type Structure (Adam Bengtsson, Mikael Bung)|
Presentation of advanced topic (proposals). This topic should be chosen and the talk should be scheduled no later than on Wednesday 21 September 13.15.
Bonus points will be given to students who have handed in homework and been prepared to present it in class (max 4 x 4 pts). Bonus points will also be given for good presentations (max 5pts) and for attendance at the presentations (max 4 x 1 pts).
The history of operational semantics by G. Plotkin.
Papers on parametric polymorphism by J. Reynolds.