This wiki page belongs to an old course instance. Please refer to the wiki for study period 1, 2017.

Types for Programs and Proofs

DAT140/DIT232, study period 1, 2015

[Note: The password to edit this page is proglog.]


Topics for the final presentation should be booked here before 15 September. You should work in groups of 3-4 people, unless having asked for an exception to work in a smaller group. Write your names after the chapter or paper you want to present or be opponents for. You may also propose a date, or say if there a date which is not possible. Presentations of chapters in the book will be scheduled early.

It is first come first serve; you may not choose a topic already chosen by others. You may also propose a research paper not in the list, but then you should discuss this with Peter or Thierry.

You can either do an Agda project and present it. Write the project theme below.

  • ... reserved by ... opponents are

Or you can present a chapter from Pierce:

  • References (Chapter 13) reserved by ... opponents are ...
  • Exceptions (Chapter 14) reserved by ... opponents are ...
  • Subtyping (Chapter 15) reserved by ... opponents are ...
  • Imperative objects (Chapter 18, depends on 13, 15) reserved by ... opponents are ...
  • Featherweight Java (Chapter 19, depends on 15) reserved by ... opponents are ...
  • Recursive types (Chapter 20) reserved by ... opponents are ...

Or you can present a classical research paper:

Some more difficult but important papers are:

  • Jean-Louis Krivine, Call-by-name lambda-calculus machine Higher Order and Symbolic Computation 20, p.199-207 (2007) (difficult!)
  • John Reynolds, Types, abstraction, and parametric polymorphism (difficult!)
  • John Reynolds, Towards a theory of type structure (difficult!)

Security types (these papers are also quite difficult)

You can also choose a paper from

Yet another possibility is to present another dependently typed language, for example

  • Coq
  • Idris reserved by Viktor Karlsson, Pontus Doverstav, Christoffer Medin, Gleb Lobanov

or proof assistant

  • Isabelle

or an article in the Stanford Encyclopedia of Philosophy

or homotopy type theory:

  • Homotopy type theory