Types for Programs and Proofs
DAT350/DIT232, study period 1, 2017
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 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
Each of these topics is supported by experimenting with the interactive
- functional programming with dependent types;
- computer-assisted interactive proving in logical
systems, including predicate logic;
- proving the correctness of functional programs;
- type systems and operational semantics for programming
There is also a Google group.
- Functional programming (essential).
- Basic knowledge of logic, including predicate logic.
- Some knowledge about programming languages.
The schedule is available in TimeEdit.
- Thursdays 10.00 - 11.45 beginning on 31 August.
- Mondays 13.15 - 15.00 beginning on 4 September.
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.
- Mondays 15.15 - 17.00 beginning on 4 September.
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.
- Take home exam: Tuesday 17 October 800 - Friday 20 October
- Presentation of advanced topic or of an Agda development.
You should work in
pairs and choose a topic no later than on Thursday 14
September 13.15. You will also be
opponents for one of the presentations. Here are some talk proposals.
Register your topic on this
Bonus points will also be given for good presentations and
opposition (max 4 pts) and
for attendance at the presentations (max 3 x 1 pts).
- Homework. Bonus points will be given to students who have
handed in homework and been prepared to present it in class (max 4 x
3 pts). The Fire system
should be used for submitting your homework. Handwritten homework
can also be handed in in class. Do not submit homework by email.
- Both presentation and take home exam are obligatory. Homework is
- Oral exam. To get the grades 4 or 5 at Chalmers, you need
to take a short oral exam.
- Linus Johansson, email@example.com
- Jacob Jonsson, firstname.lastname@example.org
- Joel Sjögren, email@example.com
- Nachiappan Valliappan, firstname.lastname@example.org