Survey Workshop on Typeful Compilation

October 9, 2000
ROPAS, KAIST
Program Organizer: Oukseh Lee

Towards a Theory of Type Structure

John C. Reynolds.
Volume 19 of Lecture Notes in Computer Science, pages 408-425, 1974.
(Presented by Hyun-Goo Kang)

Abstract

Slides

Discussion

  • it is interesting to find the meaning of types.
  • it may be possible to improve the representation of types.
  • we need to see category theory for deep understanding.
  • type is enough to encode various properties of program? other properties can be embedded into other fixpoint representation.
  • alternatives are type + alpha, lattice, constraints, model checking.

    Henk: a typed intermediate language.

    Simon Peyton Jones, Erik Meijer.
    International Workshop on Types in Compilation, 1997.
    (Presented by     Hyunjun Eo)

    Abstract

    Paper / Slides

    Discussion

  • it is beautiful, but is it necessary?
  • it was helpful to classify various system Fs and identify some terms (for example, predicative)

    Implementing Typed Intermediate Languages

    Zhong Shao, Christopher League, Stefan Monnier
    ACM International Conference on Functional Programming, pages 313-323, September 1998.
    (Presented by     Sukyoung Ryu)

    Abstract

    Recent advances in compiler technology have demonstrated the benefits of using strongly typed intermediate languages to compile richly typed source languages (e.g., ML). A type-preserving compiler can use types to guide advanced optimizations and to help generate provably secure mobile code. Types, unfortunately, are very hard to represent and manipulate efficiently; a naive implementation can easily add exponential overhead to the compilation and execution of a program. This paper describes our experience with implementing the FLINT typed intermediate language in the SML/NJ production compiler. We observe that a type-preserving compiler will not scale to handle large types unless all of its type-preserving stages preserve the asymptotic time and space usage in representing and manipulating types. We present a series of novel techniques for achieving this property and give empirical evidence of their effectiveness.

    Paper / Slides

    Discussion

  • Key idea is suspension-based \lambda encoding, hash-consing, memoization.
  • The techniques are necessary for our compiler.
    Oukseh Lee