The following three sample themes illustrate the idea of a theme:

• type soundness proofs:
  1. Milner, A Theory of Type Polymorphism in Programming
  2. Damas, Type Inference for Polymorphic References
  3. Tofte, Operational semantics and polymorphic type inference
  4. Wright & Felleisen, A Syntactic Approach to Type Soundness
  The focus of this theme is the strategy for proving the soundness of type systems, not type inference and not the problems of type inference in the presence of effects.
• hygiene in macro systems:
  1. Kohlbecker, et alii, Hygienic Macro Expansion
  2. Clinger and Rees, Macros that work
  3. Dybvig, Hieb, & Bruggeman, Syntactic abstraction in Scheme
  The focus of this them is the mechanism with which macros deal with interferences between macro substitutions and lexical scope.
• type inference and effects:
  1. Tofte, Operational semantics and polymorphic type inference
  2. Leroy and Weis, Polymorphic type inference and assignment
  3. Wright, Simple Imperative Polymorphism
  The focus of this theme is the problem of using Hindler-Milner type inference in the presence of reference cells (and other effects) and strategies for solving the problem. Do not worry about the soundness of the type systems.

Each set of quasi-citations demonstrates the kind of steps forward that research makes. Don't think other themes evolve more quickly than this. Each of the three themes ends in a paper that, in these cases, settled an issue (mostly). This doesn't have to be the case, so don't expect your favorite theme to "end"; as a matter of fact, "open" themes are a good starting point for a first paper.

Choice of theme:

I expect senior students to find two themes on their own. Specifically, I propose that you use this opportunity to learn more about the background of your dissertation topic. You are welcome, however, to choose one of the proposed themes from the list below.

Junior students may choose one of the three themes above. The price for choosing one of these themes is that you must present during one of the first three slots. Here are some other ideas for potentially interesting themes:

• early semantics of OOPLs
• types for OOPLs
• control and continuations
• control and control delimiters
• reflection derived from interpretation (3-Lisp, Brown, etc)
• Curry-Howard isomorphism
• type systems for modules
• dependent types
• abstract interpretation
• set-based analysis of programs
• lazy evaluation
• logic programming
• theorem proving
• partial evaluation
• continuations and compilation
• garbage collection
• logical frameworks

When you research the literature for your themes, keep in mind that you should find reasonably small steps and that the theme doesn't need an "end" paper. To turn the papers into a presentation, make sure that you (1) establish the connection to PL/programming and (2) bring across the necessary background; doing so may take a third of your presentation time if the theme concerns some sophisticated mathematics or implementation technique.