Recent Changes - Search:
ProgLog /

DAT350

Types for Programs and Proofs

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

SCHEDULE

Below is a preliminary schedule. Sign up by editing the wiki and writing your topic and names in one of the open slots below. You should also sign up as opponents for another talk. Please write your names after the names of the presenters as follows (Opponents: NN and NN). Each person should prepare at least one question to ask after the talk. (You can ask more if you like.)

Each slot is 20 minutes, so each presentation should last 15 minutes, leaving a few minutes for questions and changing to the next talk. If you work in pairs you should divide the time evenly between yourselves.

The goal is to be comprehensible to your fellow students. It is better to focus on some simple points and basic ideas, and present them in an understandable way, rather than try to cover everything in the chapter or article. It is also important to stick to your allotted time slot. After your talk there will be an opportunity to ask questions, first from your opponents, and then from other students.

Please send your slides to Ulf.

MONDAY 14 OCTOBER (10 slots)

  • Samuel Hammersberg and Martin Fredin - "How to Keep Your Neighbours in Order" by Connor McBride (Opponents: David Holmqvist)
  • Aparna Ram Suresh Saritha Kumari & Celestine Valan Moses - "Exceptions (Ch 14), Types and Programming Languages by Benjamin C. Pierce" (Opponents: Tim Kinderby and Hanna Schaff)
  • Praveen Alavala & Georgios Panagiotis Tsionos - Linear logic and Lazy computation
  • Matheus de Sousa Bernardo - "Subtyping (Chapter 15)" (Opponents: Anton Levinsson & Elis Kleen)
  • Anton Levinsson & Elis Kleen - "Recursive types (Chapter 20)" (Opponents: Praveen Alavala & Georgios-Panagiotis Tsionos)

THURSDAY 17 OCTOBER (5 slots)

  • Nor Führ & Erik Nygren - "Language-Based Information-Flow Security" (Opponents: Samuel Kyletoft and Enayatullah Norozi)
  • Martin Jonsson and Edvin Nilsson - "Theorems for free!" (Opponents: August Matseke & Edvin Sternvik)
  • Samuel Kyletoft and Enayatullah Norozi - Liquid Haskell (Opponents: Nor Führ and Erik Nygren)
  • Tim Kinderby and Hanna Schaff - "References (Ch 13), Types and Programming Languages by Benjamin C. Pierce" (Opponents: Aparna Ram Suresh Saritha Kumari & Celestine Valan Moses)
  • Edvin Sternvik and August Matseke - Georges Gonthier, A computer-checked proof of the Four Colour Theorem (Opponents: Martin Jonsson and Edvin Nilsson)

MONDAY 21 OCTOBER (10 slots)

  • Eli Adelhult and Jonathan Widén - "Linear types can change the world!" (Opponents: Samuel Hammersberg and Martin Fredin)
  • Rachel Samuelsson - "Elaboration with First-Class Implicit Function Types" (Opponents: August Holm & Bokun Xiao)
  • Francesco Decataldo and Ricardo Antunes - Peter Dybjer and Erik Palmgren, Intuitionistic Type Theory (Opponents: Eli Adelhult and Jonathan Widén)
  • David Holmqvist - “Types as groupoids (Homotopy type theory)" (Opponents: Rachel Samuelsson)
  • Michele Holm & William Kangas - John Launchbury, A Natural Semantics for Lazy Evaluation (Opponents: Francesco Decataldo and Ricardo Antunes)
  • August Holm & Bokun Xiao - "Natural semantics" (Opponents Aliasgar Shereef & Bilal Al Malek).
  • Imperative objects (Chapter 18) Types and Programming Languages by Benjamin C. Pierce Presenters ( Aliasgar Shereef & Bilal Al Malek).(Opponents: Matheus de Sousa Bernardo)

TALK PROPOSALS

Topics for the final presentation should be booked here on Friday 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. The available dates are (MONDAY 14 OCTOBER, THURSDAY 17 OCTOBER and MONDAY 21 OCTOBER). Please let us know if you cannot make it on any of those days, and we will take that into account when scheduling.

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 Ulf or Thierry. Yet another alternative is to 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) - Tim Kinderby & Hanna Schaff
  • Exceptions (Chapter 14) - Aparna Ram Suresh Saritha Kumari & Celestine Valan Moses
  • Subtyping (Chapter 15) - Matheus de Sousa Bernardo
  • Imperative objects (Chapter 18, depends on 13, 15) Aliasgar Shereef & Bilal Al Malek
  • 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:

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
  • C. A. R. Hoare. An axiomatic basis for computer programming.

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

  • Coq
  • Idris
  • Liquid Haskell

or proof assistant

  • Isabelle
  • Hol

or an article in the Stanford Encyclopedia of Philosophy

or homotopy type theory:

  • Homotopy type theory

or another paper: