COM 3810: Topics in Programming Languages
Instructor:
William D Clinger
Prerequisite:
COM 3357
The topic of this course is principled implementation
of programming languages and related systems. This course is
intended for PhD students who have taken the
graduate course
on programming language semantics and will be doing thesis
research in programming languages or a related area.
The course is loosely organized. We will examine a series of
case studies, taken from the research literature, that apply
semantic theory to a practical problem that arises during
implementation of a system. Each student will present a topic
or case study during class, following the examples set by the
instructor during the first lecture.
What we have done so far
- Compiler correctness;
presented by Clinger
- Will Clinger,
The topological structure of programming languages,
including a proof of correctness for a simple code generator
for the language of while loops.
- William D Clinger,
The Scheme 311 compiler: an exercise in denotational semantics,
ICFP '84.
- Joshua Guttman, Mitchell Wand, John Ramsdell, and Dino Oliva,
VLISP: A Verified Implementation of Scheme,
a special double issue of
Lisp and Symbolic Computation Volume 8, Issue 1/2, 1995.
- Asymptotic space efficiency of languages and implementations;
presented by Fabio Rojas
- Optimality and complexity of code generation;
presented by Dave Herman
- Ravi Sethi and J D Ullman,
The generation of optimal code for arithmetic expressions,
JACM 17(4), October 1970, pages 715-728.
- John Bruno and Ravi Sethi,
Code generation for a one-register machine,
JACM 23(3), July 1976, pages 502-510.
- A V Aho, S C Johnson, and J D Ullman,
Code generation for expressions with common subexpressions,
JACM 24(1), January 1977, pages 146-160.
- Soundness and complexity of Hindley-Milner type inference;
presented by Dale Vaillancourt
- Andrew Wright and Matthias Felleisen,
A syntactic approach to type soundness,
Information and Computation, ????
- Harry Mairson,
Deciding ML typability is complete for deterministic
exponential time,
POPL '90, pages 382-401.
Schedule of upcoming presentations
- 24 April:
A-normal form; presented by Greg (paper by Felleisen)
- 1 May:
Abstract interpretation; presented by Richard
(long introductory paper by Jones and Nielsen)
- 8 May:
Abstract interpretation; presented by Phillippe
(paper by Cousot, POPL 2000)
- 8 May:
Flow analysis for boxing/unboxing; presented by Ryan
- 15 May:
Partial evaluation; presented by Theo
- 15 May:
Microprocessor correctness; presented by Jaime
(three papers on the use of ACL2 to prove theorems
about the AMD K5 and K7)
- 22 May:
topic TBA; presented by Luke
- 22 May:
topic TBA; presented by PengChen
- 29 May:
topic TBA
Topics still available for presentation
- Memory management
- tagless garbage collection
- region analysis
-
Alex Aiken, Manuel Faehndrich, and Raph Levien,
Better static memory management:
Improving region-based analysis of higher-order languages,
PLDI '95
-
Mads Tofte and Jean-Pierre Talpin,
Region-based memory management,
Information and Computation, 1997
-
Mads Tofte and Lars Birkedal,
A region inference algorithm,
ACM TOPLAS 20(4), 1998
- Types
References that I don't yet want to delete from this page
- Abstract interpretation [Philippe, Richard]
Last updated 21 April 2003