Types for Programs and Proofs
DAT140/DIT232, study period 1, 2016
NewsThe take home exam will be available at 800 on Tuesday 18 October. Here is last year's exam.
Here are some more exercises in propositional logic.
Since ML1 is too small for the course, we have been assigned new lecture rooms. Unfortunately, this means that we will have different rooms on different occasions. Please consult TimeEdit.
AimThe development of powerful type systems is an important aspect of modern programming language design. This course provides an introduction to this area. In particular it introduces the notion of dependent type, a type which can depend on (is indexed by) values of another type, for example, the type of vectors indexed by its length. Dependent types are versatile. Through the Curry-Howard identification of proposition and types virtually any property of a program can be expressed using dependent types. The student will learn how to use an interactive programming system for a language with dependent types. The course is thus simultaneously an introduction to
|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 Sigma-type 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.|