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 9 OCTOBER

Arvid Rydberg && Selina Engberg, Proving Properties of Programs by Structural Induction | Opponents: Sikai Lu && Chonghan Li

Ferran Toda && Freek Geerligs, Linear logic and lazy computation. | Opponents: Arvid Rydberg && Selina Engberg

Ondrej Kubánek && Janek Stoppkotte, A formulae-as-types notion of control | Opponents: Benjamin Moosherr & Matteo Canton

Rojan Hashemi & Nazif Kadiroglu - The next 700 programming languages. | Opponents: Talha Ahmad & Armaan Rashid

Talha Ahmad && Armaan Rashid, Natural semantics | Opponents: Rojan Hashemi & Nazif Kadiroglu

Kanstantsin Nisht & Jonas Högberg, Programming in Constructive Set Theory | Opponents : Ferran Toda && Freek Geerligs

THURSDAY 12 OCTOBER

Benjamin Moosherr & Matteo Canton: Theorems for free! Opponents: Ondrej Kubánek && Janek Stoppkotte

Adam Norberg & Aline Eikeland: Call-by-name lambda-calculus machine | Opponents: Filip Torphage && Albin Aspljung

Dylan Osolian & Samuel Dahlberg: A computer-checked proof of the Four Colour Theorem | Opponents: Emelie Blade & Lucas Karlsson

Filip Torphage && Albin Aspljung: On the Mechanical evaluation of Expressions | Opponents: Anton Levinsson && Kristoffer Gustafsson

Emelie Blade & Lucas Karlsson: Idris | Opponents: Dylan Osolian & Samuel Dahlberg

MONDAY 16 OCTOBER

Sebastian Selander && Clara Salberg: A tutorial implementation of a dependently typed lambda calculus | Opponents: Kanstantsin Nisht & Jonas Högberg

Anders Berggren Sjöblom && Brage Salhus Bunk: Liquid Haskell | Opponents: Edvard Heinmetz and Gabriel Käll

Carl Bergman && Omar Zahran: Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I | Opponents: Anders Berggren Sjöblom && Brage Salhus Bunk

Evan Geng && Jonathan Lööv: Homotopy type theory (& cubical type theory) | Opponents: Sebastian Selander and Clara Salberg

Edvard Heinmetz && Gabriel Käll: Isabelle Opponents: Jessica Preiman & Anders Märak Leffler

Anton Levinsson && Kristoffer Gustafsson: A syntactic approach to type soundness | Opponents: Adam Norberg & Aline Eikeland

Felix Nilsson & Filip Nordmark - John C. Reynolds. Towards a theory of type structure | Opponents: Geng & Lööv

Jessica Preiman & Anders Märak Leffler: An axiomatic basis for computer programming. | Opponents: Carl Bergman && Omar Zahran

Sikai Lu && Chonghan Li : Linear types can change the world! | Opponents: Felix Nilsson & Filip Nordmark

Mojtaba Ataie && Philip Berg: The roots of LISP | Opponent: Nicklas Botö && Nils Jakobson Mo

Nicklas Botö && Nils Jakobson Mo: Generalizing non-linear type systems in quantum programming | Opponents: Mojtaba Ataie & Philip Berg

TALK PROPOSALS

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

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. Rojan Hashemi & Nazif Kadiroglu
  • C. A. R. Hoare. An axiomatic basis for computer programming. Jessica Preiman

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: