Types for programs and proofs

DAT350 / DIT233 Types for programs and proofs lp1 HT20 (7.5 hp), a course offered by the department of Computer Science and Engineering.

The course will be given online.

Schedule

  • Lectures:
    • Thursdays 10.00 – 11.45 beginning on 3 September: Zoom link Password: 363478;
    • Mondays 13.15 – 15.00 beginning on 7 September. Zoom link Password: 615747.
  • Exercise sessions:
    • Mondays 15.15 – 17.00 beginning on 7 September (with the same Zoom link as for the Monday lecture). This will include Agda supervision and discussion of homework. These sessions are for everyone, but in order to get credit for homework you must be prepared to present your solutions in class.

Course plan

Plan for lectures, exercise sessions and homework

Course purpose

The development of advanced type systems is an important aspect of modern programming language design. This course provides an introduction to this area. In particular it introduces dependent types, types 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.

Prerequisites:

  • Functional programming (essential).
  • Basic knowledge of logic, including predicate logic.
  • Some knowledge about programming languages.

Course literature

Agda:

Learning objectives and syllabus

  • how to program in a dependently typed functional programming language
  • how to prove theorems in a dependently typed programming language using the propositions-as-types principle
  • how to use deduction formalisms to present type systems and operational semantics of programming languages.

Link to the syllabus Chalmers
Link to the syllabus GU

Examination

Obligatory parts:

  • Take home exam: Tuesday 20 October 8.00 – Friday 23 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 Friday 18 September. Please register your topic on the wiki. You will also be opponents for one of the presentations. Here are some talk proposals. The presentations and opposition is graded and gives max 4 pts.
  • Oral exam. To get the grades 4 or 5 at Chalmers, and VG at GU, you need to take a short oral exam. This is not necessary for grade 3 at Chalmers and G at GU.

Optional parts:

  • 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 system should be used for submitting your homework. Handwritten homework can also be handed in in class. Do not submit homework by email.
  • Attendance at the presentations gives 1 point for each of the 3 presentation sessions.

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.

Contact details

  • Teachers:
    • Thierry Coquand, coquand@chalmers.se
    • Peter Dybjer, peterd@chalmers.se
    • Ulf Norell, norell@chalmers.se
  • Course evaluators: