# DAT350

[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 11 OCTOBER

1315 Liquid Haskell - Daniel Willim and Erik Ljungdahl - Opponents: Lawrence Chonavel and Beata Burreau

1335 Linear Types - Lawrence Chonavel and Beata Burreau - Opponents: Daniel Willim and Erik Ljungdahl

1415 ITT and HoTT - Axel Forsman & Artur Leitão - Opponents: Johannes Ljung Ekeroth and Lukas Skystedt

1425 *open*

THURSDAY 14 OCTOBER

1000 Recursive Types (Chapter 20) - Rasmus Thorsson and Carl Lundgren - Opponents: Daniel Stribrand and Adam Rashdan

1020 The Roots of Lisp - Daniel Stribrand and Adam Rashdan - Opponents: Sam Sohrabpour and Johan Blom

1100 Exceptions (Chapter 14) - Sam Sohrabpour and Johan Blom - Opponents: Rasmus Thorsson and Carl Lundgren

1120 Abadi - Secrecy by typing in security protocols - Anders Märak Leffler - Opponents: Erik Wallhede and Jakob Frykmer

MONDAY 18 OCTOBER

1315 Theorems for free! - Burak Yalcinkaya and Chengyuan Wang - Opponents: Anders Märak Leffler

1325 Proving properties of programs by structural induction - Johannes Ljung Ekeroth and Lukas Skystedt - Opponents: Freddy Abrahamsson and Johan Ek

1415 A computer-checked proof of the Four Colour Theorem - Erik Wallhede and Jakob Frykmer - Opponents: Burak Yalcinkaya and Chengyuan Wang

1425 Subtyping (Chapter 15) - Freddy Abrahamsson and Johan Ek - Opponents: Axel Forsman & Artur Leitão

## 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

- Agda formalization of R. M. Burstall,
*Proving properties of programs by structural induction*

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:

- John McCarthy,
*Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I* - Peter Landin,
*On the Mechanical evaluation of Expressions* - Rod Burstall,
*Proving Properties of Programs by Structural Induction* - Andrew Wright and Matthias Felleisen,
*A syntactic approach to type soundness* - Gilles Kahn,
*Natural semantics* - John Launchbury,
*A Natural Semantics for Lazy Evaluation* - Phil Wadler,
*Linear types can change the world!* - Phil Wadler,
*Theorems for free!* - Jean-Yves Girard and Yves Lafont,
*Linear logic and Lazy computation* - Georges Gonthier,
*A computer-checked proof of the Four Colour Theorem* - Paul Graham,
*The roots of LISP*fun article about the design and importance of LISP - Bengt Nordstrom,
*Programming in Martin-Lof type theory*one of the first paper explaining connections between type theory and programming - Tim Griffin,
*A formulae-as-types notion of control*a computational interpretation of classical logic, which is not supposed to exist!!

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! but fundamental**) - John Reynolds,
*Towards a theory of type structure*(**difficult!**)

Security types (these papers are also quite difficult)

- Stephan A. Zdancewic.
*Programming Languages for Information Security. PhD thesis, Cornell University, August 2002* - Andrew Myers and Andrei Sabelfeld,
*Language-Based Information-Flow Security*(survey paper on security types for information flow) - Martin Abadi,
*Secrecy by Typing in Security Protocols*(classic paper using the spi calculus) - Aleksandar Nanevski, Anindya Banerjee and Deepak Garg,
*Verification of Information Flow and Access Control Policies with Dependent Types*(a state of the art paper using dependent types for security if you're looking for something more advanced) - Martin Abadi,
*Dependency Core Calulus*

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.

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

- Thierry Coquand,
*Type Theory* - Peter Dybjer and Erik Palmgren,
*Intuitionistic Type Theory*

or homotopy type theory:

- Homotopy type theory

or another paper:

- Antonius J C Hurkens
*A Simplification of Girard's Paradox* - Andres Löh, Conor McBride, and Wouter Swierstra
*A tutorial implementation of a dependently typed lambda calculus* - Conor McBride
*How to Keep Your Neighbours in Order*