This is a graduate seminar on type refinements, a method for increasing the expressive power of type systems to track programmer-specified invariants governing persistent values and ephemeral state. For background on type refinements, please see the Triple Project web page.
All students enrolling in this course must either have completed the Programming Languages core course in the PhD program, or obtain the permission of the instructor. Competence with typed lambda calculus models of programming languages is essential, familiarity with the basics of mathematical logic and semantics is helpful.
This is a research seminar, not a lecture course. Participants are required to present one or more papers during the course of the semester. Each presentation must be accompanied in advance by typeset lecture slides in either Powerpoint or LaTeX slide format. The presenter's slides will be posted on the course web site for future reference. The presenter is responsible for presenting a summary and a critical analysis of the paper(s) assigned to her, and to lead discussion. The audience for a given paper is required to read the relevant papers in advance as preparation for the presentation.
The papers listed below represent an initial sample of the material we will cover in this class. It is to be expected that further reading will be required; the reading list will change accordingly.
Meeting time and place: Mondays and Wednesdays at 1:30PM in Porter Hall room A19C.
Please use this Powerpoint presentation template for your presentations. I recommend using TeXPoint for mathematical formulae. Please be sure to check "Embed TrueType Fonts" under the Tools Menu of the Save As dialog box!
A prototype refinement checker is now available for your use.
Last modified: Wed Dec 3 18:26:06 EST 2003