DAT140/DIT232, study period 1, 2015
[Note: The password to edit this page is proglog.]
MONDAY 10 OCTOBER
1315 References (Chapter 13): Jakob Bornecrantz, Fredrik Furufors, Timon Lapawczyk, Joacim Linder opponents are Stefanie Drerup, Jana Seep ...
1340 Exceptions (Chapter 14): Emma Gustafsson, Emma Westman, Elin Ljunggren, Hanna Materne) opponents are Johan Wermensjö, Andreas Wahlström, Linnéa Andersson, Simon Johansson
1415 Subtyping (Chapter 15): Johan Wermensjö, Andreas Wahlström, Linnéa Andersson, Simon Johansson opponents are Victor Olausson, Oskar Nyberg & William Dahlberg
1440 Recursive types (Chapter 20): Victor Olausson, Oskar Nyberg & William Dahlberg, opponents are Jakob Bornecrantz, Fredrik Furufors, Timon Lapawczyk, Joacim Linder
THURSDAY 13 OCTOBER
1000 John Launchbury, A Natural Semantics for Lazy Evaluation: Mengcheng Zhang, Amanda Lin, Jacob Rippe opponents are Oskar Abrahamsson, Konstantinos Brilakis, William Hughes, Lukas Borin
1020 Phil Wadler, Linear types can change the world!: Anton Josefsson, Björn Nordgren, Marie Klevedal and Johan Ben Mohammad opponents are Emma Gustafsson, Emma Westman, Elin Ljunggren, Hanna Materne
1105 Phil Wadler, Theorems for free!: Jan Mas, Lukas Borin and Frederik Iversen opponents are Lukas Huwald ...
1125 Jean-Yves Girard and Yves Lafont, Linear logic and Lazy computation: Oskar Abrahamsson, Konstantinos Brilakis opponents are Anton Josefsson, Björn Norén, Marie Klevedal and Johan Ben Mohammad
1140 Georges Gonthier, A computer-checked proof of the Four Colour Theorem: Jana Seep, Lukas Huwald and Stefanie Drerup opponents are ... Frederik Iversen, Christoffer Medin, Viktor Karlsson, Pontus Doverstav
MONDAY 17 OCTOBER
1315 Peter J. Landin. The next 700 programming languages: Sebastian Bellevik, Marcus Olsson, Philip Ekman, Marcus Lagerstedt) opponents are Mengcheng Zhang, Amanda Yan Lin, Jacob Rippe
1335 Idris: Viktor Karlsson, Pontus Doverstav, Christoffer Medin, opponents are Mazdak Farrokhzad, Björn Tropf, Hossein Hussain, Mushfiqur Rahman.
1410 Homotopy type theory, (Videos: HoTT: What's the Big Idea? and fresh from the oven A Functional Programmer's Guide to HoTT): Mazdak Farrokhzad, Björn Tropf, Hossein Hussain, Mushfiqur Rahman opponents are Johan Häggström, Alexandra Back, Sergio Marschall, Gleb Lobanov
1435 Grammatical Framework: Gleb Lobanov opponents are Karin Wibergh, Shamsi Abdullayev .. A. Ranta. Grammatical Framework: A Type-Theoretical Grammar Formalism. Journal of Functional Programming, 14(2), pp. 145-189, 2004.
1455 Haskell Type Functions, Fun with type functions: Karin Wibergh, Shamsi Abdullayev, opponents are Jan Mas, Sebastian Bellevik, Marcus Olsson, Philip Ekman, Marcus Lagerstedt
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 present a chapter from Pierce:
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
Yet another possibility is to present another dependently typed language, for example
or proof assistant
or an article in the Stanford Encyclopedia of Philosophy
or homotopy type theory: