ProgLog Pages 
ProgLog /
DAT350Types for Programs and ProofsDAT350/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 JeanYves 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  LanguageBased InformationFlow 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 Agdaimplementation. 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
Or you can 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:
