Types for Programs and Proofs
DAT350/DIT232, study period 1, 2017
News
Aim
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
introduction to
- 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
languages.
Each of these topics is supported by experimenting with the interactive
proof system.
Teachers
Literature
Agda:
Books:
PCF:
There is also a Google group.
Prerequisites
- Functional programming (essential).
- Basic knowledge of logic, including predicate logic.
- Some knowledge about programming languages.
Lectures
- Thursdays 10.00 - 11.45 beginning on 31 August.
- Mondays 13.15 - 15.00 beginning on 4 September.
The schedule is available in TimeEdit.
Exercise sessions
This will include Agda supervision and discussion of homework (FR, AV).
- Mondays 15.15 - 17.00 beginning on 4 September.
These exercise sessions are for everyone, but in order to get credit for homework you must be prepared to present
your solutions in class.
Examination
- Take home exam: Tuesday 17 October 800 - Friday 20 October
1200.
- 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
wiki.
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
optional.
- Oral exam. To get the grades 4 or 5 at Chalmers, you need
to take a short oral exam.
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.
Links
Course evaluators
- Linus Johansson, linusjoh@student.chalmers.se
- Jacob Jonsson, jassob@dtek.se
- Joel Sjögren, joelsjogren.wii@gmail.com
- Nachiappan Valliappan, nacval@student.chalmers.se