|
     
| |
TAL Papers
 | Dan Grossman and Greg Morrisett.
Scalable Certification for Typed Assembly Language.
In the 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal,
Canada, September 2000.
(abstract, pdf, ps)
|
|
| Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to
Typed Assembly Language. In ACM Transactions on Programming Languages
and Systems, 21(3):528-569, May 1999.
(abstract, dvi,
pdf, ps.gz) |
| Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith,
David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A Realistic Typed
Assembly Language. In the 1999 ACM SIGPLAN Workshop on Compiler Support for
System Software, pages 25-35, Atlanta, GA, USA, May 1999.
(abstract, dvi, pdf, ps.gz) |
| Neal Glew and Greg Morrisett. Type-Safe Linking and Modular Assembly Language.
In the Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages
250-261, San Antonio, TX, USA, January 1999.
(abstract, dvi, pdf, ps.gz) |
| Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-Based Typed Assembly
Language. In the 1998 Workshop on Types in Compilation, Kyoto, Japan, March 1998.
Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer
Science, volume 1473, pages 28-52. Springer-Verlag, 1998.
(abstract, dvi,
pdf, ps.gz) |
| Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed
Assembly Language. In the Twenty-Fifth ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 85-97, San Diego, CA, USA, January 1998.
(abstract, dvi,
pdf, ps.gz) |
Related Papers
 |
Frederick Smith, Dan Grossman, Greg Morrisett, Luke Hornof,
Trevor Jim. Compiling for Runtime Code Generation.
Submitted for publication, October 2000.
(abstract, dvi,
pdf, ps) |
| David Walker and Greg Morrisett. Alias
Types for Recursive Data Structures. Submitted for
publication, March 2000.
(abstract, pdf,
ps.gz) |
| Karl Crary, Michael Hicks and Stephanie Weirich. Safe and
Flexible Dynamic Linking of Native Code.
In the 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal,
Canada, September 2000.
(abstract, ps.gz) |
|
| Frederick Smith, David Walker and Greg Morrisett. Alias
Types. In European Symposium on Programming,
Berlin, Germany, March 2000.
(abstract, pdf, ps.gz) |
| Karl Crary and Stephanie Weirich. Resource Bound Certification.
In the Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
pages 184-198, Boston, MA, USA, January 2000.
(abstract, dvi, pdf,
ps.gz) |
| David Walker. A Type System for Expressive Security Properties.
In the Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
pages 254-267, Boston, MA, USA, January 2000.
(abstract, pdf,
ps.gz)
A previous version of this paper appeared in the FLOC'99 Workshop on Run-time Result
Verification, Trento, Italy, July 1999.
(abstract, pdf, ps.gz) |
| Karl Crary. A Simple Proof Technique for Certain Parametricity Results.
In the 1999 ACM SIGPLAN International Conference on Functional
Programming, pages
82-89, Paris, France, September 1999.
(abstract, dvi, pdf, ps.gz) |
| Karl Crary and Stephanie Weirich. Flexible Type Analysis.
In the 1999 ACM SIGPLAN International Conference on Functional Programming., pages
233-248, Paris, France, September 1999.
(abstract, dvi, pdf, ps.gz) |
| Neal Glew. Type Dispatch for Named Hierarchical Types. In the 1999
ACM SIGPLAN International Conference on Functional Programming, pages 172-182, Paris, France,
September 1999.
(abstract, dvi, pdf, ps.gz) |
| Neal Glew. Object Closure Conversion. In the 3rd
International Workshop on Higher Order Operational Techniques in Semantics, Paris,
France, September 1999.
(abstract, dvi,
pdf, ps.gz) |
| Steve Zdancewic, Dan Grossman, and Greg Morrisett. Principals in
Programming Languages: A Syntactic Proof Technique. In the 1999
ACM SIGPLAN International
Conference on Functional Programming, pages 197-207, Paris, France, September 1999.
Winner of "Best Paper" at PLI99.
(abstract, dvi, pdf, ps) |
| Luke Hornof and Trevor Jim. Certifying Compilation and Run-time Code
Generation. In the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program
Manipulation, San Antonio, TX, USA, January 1999.
(abstract, pdf,
ps.gz) |
| Karl Crary, David Walker, and Greg Morrisett. Typed Memory Management in a Calculus
of Capabilities. In Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 262-275, San Antonio, TX, USA, January 1999.
(abstract, dvi, pdf, ps.gz) |
| Frederick Smith and Greg Morrisett. Comparing Mostly-Copying and
Mark-Sweep Conversative Collection. In 1998 International
Symposium on Memory Management, pages 68-78, Vancouver, Canada, October 1998.
(abstract, pdf,
ps.gz) |
| Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in
Type-Erasure Semantics. 1998 International Conference on Functional Programming,
pages 301-312, Baltimore, September 1998.
(abstract, dvi,
pdf, ps.gz) |
Technical Reports
| Frederick Smith, Dan Grossman, Greg Morrisett, Luke Hornof,
Trevor Jim. Compiling for Runtime Code Generation (Extended
Version). Technical Report TR2000-1824, Cornell University,
October 2000.
(abstract, dvi,
pdf, ps) |
| David Walker and Greg Morrisett. Alias Types for Recursive
Data Structures.
Technical Report TR2000-1787, Cornell University, March 2000.
(abstract, pdf,
ps.gz) |
| David Walker, Karl Crary and Greg Morrisett. Typed Memory
Management in a Calculus of Capabilities. Technical Report
TR2000-1780, Cornell University, February 2000.
(abstract, dvi,
pdf, ps.gz) |
| Dan Grossman and Greg Morrisett. Scalable Certification of
Native Code: Experience from Compiling to TALx86.
Technical Report TR2000-1783, Cornell University, February 2000.
A
TIC00 paper is a revision of this report; please refer to that
paper.
(abstract, pdf,
ps) |
| Frederick Smith, David Walker and Greg Morrisett. Alias Types.
Technical Report TR99-1773, Cornell University, October 1999.
(abstract, pdf,
ps.gz) |
| Neal Glew. Object Closure Conversion. Technical Report
TR99-1763, Cornell University, August 1999.
(abstract, dvi, pdf, ps.gz) |
| Steve Zdancewic and Dan Grossman. Principals in Programming Languages:
Technical Results. Technical Report TR99-1752, Cornell University, June
1999.
(abstract, dvi,
pdf, ps) |
| David Walker. A Type System for Expressive Security Policies.
Technical Report TR99-1740, Cornell University, April 1999.
(abstract, pdf, ps.gz) |
| Neal Glew. Type Dispatch for Named Hierarchical Types.
Technical Report TR99-1738, Cornell University, April 1999.
(abstract, dvi,
pdf, ps.gz) |
| Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-Based Typed Assembly
Language (Extended version). Technical Report CMU-CS-98-178, Carnegie Mellon
University, December 1998.
(abstract, dvi,
pdf, ps.gz) |
| Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in
Type-Erasure Semantics (Extended version). Technical Report TR98-1721, Cornell
University, November 1998.
(abstract, dvi, pdf, ps.gz) |
| Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed
Assembly Language (Extended version). Technical Report TR97-1651, Cornell University,
November 1997.
(abstract, dvi, pdf, ps.gz) |
| Frederick Smith and Greg Morrisett. Mostly-Copying Collection: A Viable
Alternative to Conversative Mark-Sweep. Technical Report TR97-1644, Cornell
University, August 1997.
(abstract, pdf, ps.gz) |
|
