DAT140
This wiki page belongs to an old course instance. Please refer to the wiki for study period 1, 2017.
Types for Programs and Proofs
DAT140/DIT232, study period 1, 2015
[Note: The password to edit this page is proglog.]
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 do an Agda project and present it. Write the project theme below.
- ... reserved by ... opponents are
Or you can present a chapter from Pierce:
- References (Chapter 13) reserved by ... opponents are ...
- Exceptions (Chapter 14) reserved by ... opponents are ...
- Subtyping (Chapter 15) reserved by ... opponents are ...
- Imperative objects (Chapter 18, depends on 13, 15) reserved by ... opponents are ...
- Featherweight Java (Chapter 19, depends on 15) reserved by ... opponents are ...
- Recursive types (Chapter 20) reserved by ... opponents are ...
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
- 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
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)
- 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)
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 reserved by Viktor Karlsson, Pontus Doverstav, Christoffer Medin, Gleb Lobanov
or proof assistant
- Isabelle
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