Recent Changes - Search:

ProgLog Main


ProgLog Pages


edit SideBar

DAT350

Types for Programs and Proofs

DAT350/DIT232, study period 1, 2017

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


PRELIMINARY SCHEDULE

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!

MONDAY 9 OCTOBER

1315 References (Chapter 13) reserved by Gunther Bidlingmaier (open for a 2nd person) opponents are Jim Bengtsson/Albin Garpetun

1330 Exceptions (Chapter 14) reserved by Jim Bengtsson/Albin Garpetun opponents are Jimmy Holdö/David Ådvall

1345 Featherweight Java (Chapter 19, depends on 15) reserved by Andreas Ekeroot/Jacob Jonsson opponents are Björn Åhlander/Johan Gerdin

1405 Recursive types (Chapter 20) reserved by Jimmy Holdö/David Ådvall opponents are Gunther Bidlingmaier (open for a 2nd person)

1420 John McCarthy, Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I -- reserved by Linus Johansson/Gustav Örtenberg opponents are Andreas Ekeroot/Jacob Jonsson

1435 Coq reserved by Mauricio Chimento, opponents are Pierre Kraft & Edvard Hübinette

1450 Liquid Haskell by Andreas Källberg, Henrik Rostedt, opponents are Mauricio Chimento

THURSDAY 12 OCTOBER

1000 Subtyping (Chapter 15) reserved by Alexander Sjösten/Anton Ekblad (date must be October 12) opponents are Joel Sjögren & Leon Bohn

1015 Phil Wadler, Linear types can change the world! reserved by Joel Sjögren & Leon Bohn opponent is Anders Märak Leffler & Mickel Hoang

1030 Phil Wadler, Theorems for free! reserved by Frederik Ramcke opponents are Andreas Källberg, Henrik Rostedt

1100 Jean-Yves Girard and Yves Lafont, Linear logic and Lazy computation reserved by Juan Ricart and Clémence Mertz opponent is Frederik Ramcke

1115 Bernardy, Boespflug, Newton, Peyton Jones, Spiwack: Retrofitting Linear Types. Reserved by Edvard Hübinette Pierre Kraft opponents are Nachiappan V (open for a 2nd person)

1130 Proof of graph algorithm properties (BFS, Dijkstras, or similar) reserved by Micke Hoang/Elias Forsberg (date cannot be October 16, would suggest October 12) opponents are Linus Johansson and Gustav Örtenberg

1145 Agda formalisation of the proofs in Pfenning and Davies, A Judgemental Reconstruction of Modal Logic reserved by Maximilian Algehed - opponents are Anton Ekblad and Alexander Sjösten.

MONDAY 16 OCTOBER

1315 Peter Landin, On the Mechanical evaluation of Expressions -- reserved Jakob Larsson and David Mebus opponents are Erik Sjöström and Fredrik Thune (Can only present on 16/10)

1330 Myers & Sabelfeld - Language-Based Information-Flow Security reserved by Anders M.L. and Juan Pablo Contreras opponent is Maximilian Algehed and Tobias Rastemo

1345 A Natural Semantics for Lazy Evaluation (prefers 16 October) reserved by Erik Sjöström and Fredrik Thune opponents are Elias Forsberg.

1400 Siavash & Nachiappan - will also present the above paper, but with some Agda-implementation. Opponent is Juan Pablo Contreras

1420 Newbern - All About Monads, implementation and proofs of basic monads reserved by Johan Gerdin and Björn Åhlander opponents are Alija Bihorac/Bekim Rabushaj.

1435 Proof of sorting algorithm "MergeSort" on lists of natural numbers, reserved by Alija Bihorac/Bekim Rabushaj. Opponents are Siavash Hamedani & Oskar Rutqvist

1450 Rational numbers and some interesting properties and theorems regarding them, reserved by Tobias Rastemo and Oskar Rutqvist. Opponents are Jakob Larsson and David Mebus

TALK PROPOSALS

Topics for the final presentation should be booked here on the 14 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 9 OCTOBER, THURSDAY 12 OCTOBER or MONDAY 16 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

  • ... reserved by ... opponents are
  • Proof of graph algorithm properties (BFS, Dijkstras, or similar) reserved by Micke Hoang/Elias Forsberg (date cannot be October 16, would suggest October 12) opponents are Linus Johansson and Gustav Örtenberg
  • Newbern - All About Monads, implementation and proofs of basic monads reserved by Johan Gerdin and Björn Åhlander opponents are Alija Bihorac/Bekim Rabushaj.
  • Myers & Sabelfeld - Language-Based Information-Flow Security reserved by Anders M.L. and Juan P. C. F. opponent is Maximilian Algehed (prefers late presentation; in particular not on the 9th)
  • Siavash & Nachiappan - John Launchbury, A Natural Semantics for Lazy Evaluation (prefers 16 October) reserved by Erik Sjöström and Fredrik Thune opponents are Elias Forsberg & Micke Hoang
  • Proof of sorting algorithm "MergeSort" on lists of natural numbers, reserved by Alija Bihorac/Bekim Rabushaj. Opponents are ...
  • Rational numbers and some interesting properties and theorems regarding them, reserved by Tobias Rastemo and Oskar Rutqvist

Or you can present a chapter from Pierce:

  • References (Chapter 13) reserved by Gunther Bidlingmaier (MONDAY 9 OCTOBER, open for a 2nd person) opponents are ...
  • Exceptions (Chapter 14) reserved by Jim Bengtsson/Albin Garpetun opponents are ...
  • Subtyping (Chapter 15) reserved by Alexander Sjösten/Anton Ekblad (date must be October 12) opponents are ...
  • Imperative objects (Chapter 18, depends on 13, 15) reserved by ... opponents are ...
  • Featherweight Java (Chapter 19, depends on 15) reserved by Andreas Ekeroot/Jacob Jonsson opponents are ...
  • Recursive types (Chapter 20) reserved by Jimmy Holdö/David Ådvall 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 reserved by Mauricio Chimento, opponents are ...
  • Idris reserved by Viktor Karlsson, Pontus Doverstav, Christoffer Medin, Gleb Lobanov
  • Liquid Haskell by Andreas Källberg, Henrik Rostedt, opponents are ...

or proof assistant

  • Isabelle

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 15, 2017, at 10:10 AM