Types and Programming Languages book cover

Types for Programs and Proofs

DAT350/DIT232, study period 1, 2018


  • We have now corrected the take home exam, and also held the oral exams for grade 4 and 5. The results will be registered shortly.


    The 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) variables of other types. For example, the type of vectors is indexed by its length. Dependent types are versatile. Through the Curry-Howard identification of propositions 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 Each of these topics is supported by experimenting with the interactive proof system.


    The schedule is available in TimeEdit.

    Plan for lectures, exercise sessions and homework

    Exercise sessions

    This will include Agda supervision and discussion of homework (FR, AV). These exercise sessions are for everyone, but in order to get credit for homework you must be prepared to present your solutions in class.



    Agda: Books: PCF:



    Note that both homework and take home exam should be done individually. If we find out that people have helped each other or copied solutions, we will fail the whole course both for the helper and the helped.


    Course evaluators