Your task is to make a presentation with slides (latex, powerpoint,
You can either choose to present a chapter from Pierce or a research
paper in the area of type system. This year we will introduce yet
another option: to carry out an Agda development and present
it to the class.
You should do your best to convey as much interesting information
about the topic as possible in the short time given to you. Try to
pitch it at the right level so that your fellow students will be able
to follow the presentation.
You should work in pairs, and you should divide the presentation
between each other.
Here are some suitable chapters from Pierce:
And here are some classical research papers:
- 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)
Some more difficult but important papers are:
- 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 computaton
- Security types.
- Georges Gonthier, A computer-checked proof of the Four Colour Theorem.
- Jean-Louis Krivine, Call-by-name lambda-calculus machine Higher Order and Symbolic
Computation 20, p.199-207 (2007)
- John Reynolds,
Types, abstraction, and parametric polymorphism
- John Reynolds, Towards a
theory of type structure
Other topics in the general
area of type systems are also welcome, but please discuss with us if
you want to present a paper which is not listed above! For example,
many of the
listed by Benjamin Pierce would be
suitable for presentation.