# DAT350

# Types for Programs and Proofs

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

## SCHEDULE

Each presentation should last 15 minutes. 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 Peter.

MONDAY 14 OCTOBER

- References (Chapter 13) [talk: Patrick Wadström] [opponents: Adam Fredriksson & Gustav Lahti]
- Exceptions (Chapter 14) [talk: Jonathan Krän & Molly Skelbye][opponents: Thomas Li & Ari von Nordenskjöld]
- Recursive types (Chapter 20) [talk: Therese Andersson] [opponents: Johan Ekdahl & Edwin Peng]
- John McCarthy,
*Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I*[talk: Thomas Li & Ari von Nordenskjöld][opponents: Oskar Vigren & Daniel Heurlin] - Peter Landin,
*On the Mechanical evaluation of Expressions*[talk: Oskar Vigren & Daniel Heurlin] [opponents: Angelica Strandberg and Philip Svensson]

THURSDAY 17 OCTOBER

- Rod Burstall,
*Proving Properties of Programs by Structural Induction*[talk: Arianna Masciolini & Jan Eisenmenger] [opponents: Jonathan Krän & Molly Skelbye] - Andrew Wright and Matthias Felleisen,
*A syntactic approach to type soundness*[talk: Johan Ekdahl & Edwin Peng] [opponents: Arianna Masciolini & Jan Eisenmenger] - Gilles Kahn,
*Natural semantics*- Adam Fredriksson & Gustav Lahti [opponents: David Lidell & Francesco Gazzetta] - John Launchbury,
*A Natural Semantics for Lazy Evaluation*[talk: Angelica Strandberg and Philip Svensson] , Opponents: Karl Lennartsson & Riccardo Zanetti - Per Martin-Löf, "Constructive Mathematics and Computer Programming" [talk: Warrick Macmillan]

MONDAY 21 OCTOBER

- Phil Wadler,
*Theorems for free!*- Christian Persson and Simon Sundström [opponent: Samuel Holgersson] - Georges Gonthier,
*A computer-checked proof of the Four Colour Theorem*talk:Sven Hellsten [opponents: Björn Larsson] - Jean-Louis Krivine,
*Call-by-name lambda-calculus machine*Higher Order and Symbolic Computation 20, p.199-207 (2007) [talk: Karl Lennartsson & Riccardo Zanetti] [opponents: Simon Sundström & Christian Persson] - Homotopy type theory [talk: David Lidell & Francesco Gazzetta][opponent: Warrick Macmillan]
- Jean-Yves Girard and Yves Lafont,
*Linear logic and Lazy computation*[talk: Björn Larsson] [opponents: Patrick Wadström] - Martin Abadi,
*Secrecy by Typing in Security Protocols*[talk: Samuel Holgersson] [opponent: Sven Hellsten]

## TALK PROPOSALS

Topics for the final presentation should be booked here on Friday the 20 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 14 OCTOBER, THURSDAY 17 OCTOBER and MONDAY 21 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 Peter or Thierry. Yet another alternative is to do an Agda project and present it. Write the project theme below.

Agda project themes

Or you can present a chapter from Pierce:

- References (Chapter 13) [talk: Patrick Wadström]
- Exceptions (Chapter 14) [talk: Jonathan Krän & Molly Skelbye]
- Subtyping (Chapter 15)
- Imperative objects (Chapter 18, depends on 13, 15)
- Featherweight Java (Chapter 19, depends on 15)
- Recursive types (Chapter 20) [talk: Therese Andersson]

Or you can present a classical research paper:

- John McCarthy,
*Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I*[talk: Thomas Li & Ari von Nordenskjöld] - Peter Landin,
*On the Mechanical evaluation of Expressions*[talk: Oskar Vigren & Daniel Heurlin] - Rod Burstall,
*Proving Properties of Programs by Structural Induction*[talk: Arianna Masciolini & Jan Eisenmenger] - Andrew Wright and Matthias Felleisen,
*A syntactic approach to type soundness*[talk: Johan Ekdahl & Edwin Peng] - Gilles Kahn,
*Natural semantics*- Adam Fredriksson & Gustav Lahti - John Launchbury,
*A Natural Semantics for Lazy Evaluation*- Angelica Strandberg and Philip Svensson - Phil Wadler,
*Theorems for free!*- Christian Persson and Simon Sundström - Jean-Yves Girard and Yves Lafont,
*Linear logic and Lazy computation*[talk: Björn Larsson] - Georges Gonthier,
*A computer-checked proof of the Four Colour Theorem*talk:Sven Hellsten

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!**) [talk: Karl Lennartsson & Riccardo Zanetti] - 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)

- 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 [talk: David Lidell & Francesco Gazzetta]