2008 (for 1998):
From System F to Typed
Assembly Language, Greg Morrisett, David Walker, Karl Crary, and Neal
Glew
Citation
"From System F to Typed
Assembly Language" by Greg Morrisett, David
Walker, Karl Crary, and Neal Glew began a major development in the
application of type system ideas to low level programming. The paper shows
how to compile a high-level, statically typed language into TAL, a typed
assembly language defined by the authors. The type system for the assembly
language ensures that source-level abstractions like closures and
polymorphic functions are enforced at the machine-code level while
permitting aggressive, low-level optimizations such as register allocation
and instruction scheduling. This infrastructure provides the basis for
ensuring the safety of untrusted low-level code artifacts, regardless of
their source. A large body of subsequent work has drawn on the ideas in
this paper, including work on proof-carrying code and certifying compilers.
2007 (for 1997):
Proof-carrying Code,
George Necula
2006 (for 1996):
Points-to Analysis in
Almost Linear Time,
Bjarne Steensgaard
2005 (for 1995):
A Language with
Distributed Scope, Luca Cardelli
2004 (for 1994):
Implementation of the Typed Call-by-Value lambda-calculus using a Stack of
Regions, Mads Tofte and
Jean-Pierre Talpin
2003 (for 1993): Imperative
functional programming,
Simon Peyton Jones
and Philip Wadler.
