[Prev][Next][Index][Thread]

Re: Seeking Papers on Type-Directed Compilation

Hello,

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.

-Oukseh Lee

--
(*
  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
interest (http://www.doc.ic.ac.uk/~clh/Papers/index.html):

 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
http://types.bu.edu/comp-flow-types.html

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
page:

http://oak.bc.edu/~muller/papers.html

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
your list.

(* 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
    Dominic Duggan

--
 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
 Alias Types
    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

--
END