Re: Seeking Papers on Type-Directed Compilation
A few weeks ago, I sent an e-mail which requested papers related to
compilation with types, or type-directed compilation.
Thanks for kind replied mails.
I summarized the contents of the replied mails.
It is my original list.
From System F to Typed Assembly Language
G. Morrisett et al. TOPLAS 99
A Type-Based Compiler for Standard ML
Z. Shao, A. W. Appel, PLDI 95
TIL: a Type-Directed Optimizing Compiler for ML
D. Tarditi et al. PLDI 96
Towards a Theory of Type Structure
J. C. Reynolds, LNCS 74
Henk: a Typed Intermediate Language
S. Peyton-Jones, E. Meijer, TIC 97
Implementing Typed Intermediate Languages
Z. Shao, C. League, S. Monnier, ICFP 98
Typed Closure Conversion
Y. Minamide, G. Morrisett, R. Harper, POPL 96
Typed Closure Conversion for Recursively-Defined Functions
G. Morrisett, R. Harper, HOOTS 98
Unboxed Values As First Class Citizens
S. L. Peyton-Jones, J. Launchbury, FPCA 91
Unboxed Objects and Polymorphic Typing
X. Leroy, POPL 92
Formally Optimal Boxing
F. Henglein, J. Jorgensen, POPL 94
Flexible Representation Anaysis
Z. Shao, ICFP 97
The Effectiveness of Type-Based Unboxing
X. Leroy, TIC 97
Compiling Polymorphism Using Intensional Type Analysis
R. Harper, G. Morrisett, POPL 95
Intensional Polymorphism in Type-Erasure Semantics
K. Crary, S. Weirich, G. Morrisett, ICFP 98
Flexible Type Analysis
K. Crary, S. Weirich, ICFP 99
Fully Reflexive Intensional Type Analysis in Type Erasure Semantics
B. Saha, V. Trifonov, Z. Shao, TIC 00
Explicit Polymorphism and CPS Conversion
R. Harper, M. Lillibridge, POPL 93
Tag-Free Garbage Collection Using Explicit Type Parameters
A. Tolmach, LFP 1994
Stack-Based Typed Assembly Language
G. Morrisett, K. Crary, N. Glew, D. Walker, TIC 98
Type-Safe Linking and Modular Assembly Language
N. Grew, G. Morrisett, POPL 99
TALx86: A Realistic Typed Assembly Language
G. Morriestt et al. CSSE 99
Garbage Collection Based on Linear Type System
A. Igarashi, N. Kobayashi, TIC 00
And the followings are recommended papers. -Oukseh
some of chris hankin's papers on type based static analysis might be of
Deriving algorithms from type inference systems: Application to
strictness analysis, POPL'94, ACM Press (with D. Le Metayer)..
Lazy type inference for the strictness analysis of lists,
ESOP'94, LNCS 788 (with D. Le Metayer)..
A type-based framework for program analysis, SAS'94, LNCS 864
(with D. Le Metayer)..
Lazy Type Inference and Program Analysis, Science of Computer
Programming, Vol 25, 1995 (with D. Le Metayer)..
I reccomend you to visit
Hello Oukseh, You'll find many papers on the topic on the
Church Project web page (http://types.by.edu/Home.html).
You can also find many of these by looking at my papers
Enclosed below is a portion cut from the web page at
<URL:http://www.cee.hw.ac.uk/~jbw/papers/> which should be included in
(* I got some papers from those sites. -Oukseh *)
Space issues in compiling with intersection and union types.
Allyn Dimock et al., TIC 2000.
A calculus for link-time compilation
Elena Machkasova and Franklyn Turbak, 2000.
Compiling with polymorphic and polyvariant flow types.
Franklyn Turbak et al., TIC 1997.
A typed intermediate language for flow-directed compilation.
J. B. Wells et al.,
Joint Conf. Theory & Practice of Software Development, 1997.
Strongly typed flow-directed representation transformations.
Allyn Dimock et al., Conf. Functional Programming, 1997.
A calculus with polymorphic and polyvariant flow types.
J. B. Wells et al., JFP (to appear)
You may be interested to look at the proceedings of the 2000 Workshop on
Types in Compilation, to be held next week in Montreal. The workshop has a
variety of papers on the latest work in the area. The proceedings are
available as a CMU technical report numbered CMU-CS-00-161.
(* Also I got some papers from that site.
I don't display a paper if it is redundant. -Oukseh *)
Scalable Certification for Typed Assembly Language
Dan Grossman, Greg Morrisett
Safe and Flexible Dynamic Linking of Native Code
Michael Hicks, Stephanie Weirich, Karl Crary
Sharing in Typed Module Assembly Language
Semantics of Memory Management for Polymorphic Languages
Morrisett and Harper
Type Memory Management in a Capability Calculus
K Crary, D Walker, and G Morrisett, POPL 99
A Type-Theoretic Interpretation of Standard ML
Harper and Stone
Deciding Type Equivalence in a Language with Singleton Kinds
Stone and Harper
Object Closure Conversion
Neal Glew, HOOTS 99
Type Dispatch for Named Hierarchical Types
Neal Glew, ICFP 99
Alias Types for Recursive Datastructures
D Walker and G Morrisett, TIC 00
F Smith, D Walker, and G Morrisett, ESOP 00
Region-Based Memory Management
Mads Tofte and Jean-Pierre Talpin
From Region Inference to von Neumann Machines
via Region Representation Inference
L. Birkedal and M. Tofte and M. Vejlstrup