Types for Programs and Proofs
DAT350/DIT232, study period 1, 2018
News
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.
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 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
- 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.
Lectures
- Thursdays 10.00 – 11.45 beginning on 6 September.
- Mondays 13.15 – 15.00 beginning on 10 September.
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).
- Mondays 15.15 – 17.00 beginning on 10 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.
Teachers
Literature
Agda:
Books:
PCF:
Prerequisites
- Functional programming (essential).
- Basic knowledge of logic, including predicate logic.
- Some knowledge about programming languages.
Examination
- Take home exam: Tuesday 23 October 8.00 – Friday 26 October
12.00.
- Presentation of advanced topic or of an Agda development.
You should work in
pairs and choose a topic no later than on Thursday 20
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, 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
- Tobias Andersson, tobande@student.chalmers.se
- Robert Krook, guskrooro@student.gu.se
- Heyu Qin, heyu@student.chalmers.se
- Ayberk Tosun, ayberk@student.chalmers.se