Recent Changes - Search:

ProgLog Main


ProgLog Pages


edit SideBar

DAT140

Types for Programs and Proofs

DAT140/DIT232, study period 1, 2015

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


SCHEDULE

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

TALK PROPOSALS

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:

  • References (Chapter 13) reserved by (Jakob Bornecrantz, Fredrik Furufors, Timon Lapawczyk ...) opponents are ...
  • Exceptions (Chapter 14) reserved by (Emma Gustafsson, Emma Westman, Elin Ljunggren, Hanna Materne) opponents are ...
  • Subtyping (Chapter 15) reserved by (Johan Wermensjö, Andreas Wahlström, Linnéa Andersson) opponents are ...
  • Imperative objects (Chapter 18, depends on 13, 15) reserved by ... opponents are ...
  • Featherweight Java (Chapter 19, depends on 15) reserved by (Johan Häggström, Alexandra Back, Sergio Marschall) opponents are ...
  • Recursive types (Chapter 20) reserved by (Victor Olausson, Victor Nilsson, Oskar Nyberg & William Dahlberg) opponents are (Jakob Bornecrantz, Fredrik Furufors, ...)

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
  • Idris reserved by Viktor Karlsson, Pontus Doverstav, Christoffer Medin, Gleb Lobanov

or proof assistant

  • Isabelle

or an article in the Stanford Encyclopedia of Philosophy

or homotopy type theory:

  • Homotopy type theory reserved by Mazdak Farrokhzad, Björn Tropf, Hossein Hussain, Mushfiqur Rahman
Edit - History - Print - Recent Changes - Search
Page last modified on October 17, 2016, at 09:14 AM