Recent Changes - Search:

ProgLog Main

ProgLog Pages

edit SideBar


Types for Programs and Proofs

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


Please plan a 10 minute talk where each presenter speaks for 5 minutes each. Plan for a 2 minute opposition, and 3 minutes for a break before the next talk. It's a short time, it will have to be an "appetiser" talk where you focus on the essentials. Remember that the quality of the talk is proportional to how much the audience can get out of it. Try to keep things simple, and stick to your slot!


1315 Tobias J. Andersson & Fabian Krause - References(Chapter 13) - Opposing: Sarosh Nasir & Henry Ly

1335 Simon Petersson - Exceptions (Chapter 14) - Opposing: Davide Donato & Heyu Qin

1405 Simon Alling & Denis Furian - Subtyping (Chapter 15) Opponents: Elin Björnsson & Miki Swahn

1425 Sarosh Nasir & Henry Ly - Imperative objects (Chapter 18)

  Opposing - Robert Krook & Therese Andersson

1445 Elin Björnsson & Miki Swahn - Natural semantics Opponent: Simon Petersson


1000 - Davide Donato & Heyu Qin - A Natural Semantics for Lazy Evaluation Opponents: Tobias Andersson & Fabian Krause

1020 - Joel Hultin & Eric Olsson - A computer-checked proof of the Four Colour Theorem

  Opposing - Victor Risne & Martin Sigvardsson

1050 - Robert Krook & Therese Andersson - Linear types can change the world

  Opposing - Joel Hultin & Eric Olsson

1110 - Stefan Marton & Olof Düsterdieck - Retrofitting Linear Types Opponent: Sven Hellsten

1130 - Rahel Ahmed - Hol [Opponent: Ayberk Tosun]


1315 - Sven Hellsten, Recursive types - Opposing: Johan Johansson & David Hagerman Olzon

1335 - Johan Johansson & David Hagerman Olzon - On the Mechanical evaluation of Expressions — opponents: Simon Alling and Denis Furian

1405 - Ayberk Tosun - A Formulae-as-type Notion of Control [opponent: Jannis Limperg]

1425 - Victor Risne & Martin Sigvardsson - Linear logic and Lazy computation Opponents: Stefan Marton & Olof Düsterdieck

1445 - Jannis Limperg - Coq [opponent: Rahel Ahmed]


Topics for the final presentation should be booked here on the 20 September at the latest. You should work in pairs, unless having asked for an exception to work alone. Write your names after the chapter or paper you want to present or be opponents for. You may also propose a date, (MONDAY 15 OCTOBER, THURSDAY 18 OCTOBER or MONDAY 22 OCTOBER). 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.

Agda project themes

Or you can present a chapter from Pierce:

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

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 Benjamin Pierce's list of great papers on programming languages

  • Peter J. Landin. The next 700 programming languages.

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

  • Coq [talk: Jannis Limperg]
  • Idris
  • Liquid Haskell

or proof assistant

  • Isabelle
  • Hol [talk: Rahel Ahmed]

or an article in the Stanford Encyclopedia of Philosophy

or homotopy type theory:

  • Homotopy type theory
Edit - History - Print - Recent Changes - Search
Page last modified on October 16, 2018, at 11:23 AM