Talk proposals
Your task is to make a presentation with slides (latex, powerpoint,
...)
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
roughly equally
between each other.
You can either 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
- Andrew Wright and Matthias Felleisen, A syntactic approach to type soundness
- Gilles Kahn, Natural semantics
- John Launchbury, A Natural Semantics for Lazy Evaluation
- Rod Burstall, Proving properties of programs by structural induction
- Phil Wadler and Robby Findler, Well-typed programs cannot be
blamed
- Phil Wadler, Linear types can change the world!
- Phil Wadler, Theorems for free!
- Jean-Yves Girard and Yves Lafont, Linear
logic and lazy computaton
- Coq?
- Isabelle?
- Security types.
- 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)
- 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.