Types in Compilation

third International Workshop, TIC 2000 Montreal, Canada, September 21, 2000 Revised Selected Papers

  • Robert┬áHarper
Conference proceedings TIC 2000

Part of the Lecture Notes in Computer Science book series (LNCS, volume 2071)

Table of contents

  1. Front Matter
    Pages I-XII
  2. Types in Compilation

    1. Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, J. B. Wells, Jeffrey Considine
      Pages 27-52
    2. Dominic Duggan
      Pages 85-116
    3. Dan Grossman, Greg Morrisett
      Pages 117-145
    4. Michael Hicks, Stephanie Weirich, Karl Crary
      Pages 147-176
    5. David Walker, Greg Morrisett
      Pages 177-206
  3. Back Matter
    Pages 207-207

About these proceedings


The importance of typed languages for building robust software systems is, by now, an undisputed fact. Years of research have led to languages with richly expressive, yet easy to use, type systems for high-level programming languages. Types provide not only a conceptual framework for language designers, but also a ord positive bene ts to the programmer, principally the ability to express and enforce levels of abstraction within a program. Early compilers for typed languages followed closely the methods used for their untyped counterparts. The role of types was limited to the earliest s- ges of compilation, and they were thereafter ignored during the remainder of the translation process. More recently, however, implementors have come to - cognize the importance of types during compilation and even for object code. Several advantages of types in compilation have been noted to date: { They support self-checking by the compiler. By tracking types during c- pilation it is possible for an internal type checker to detect translation errors at an early stage, greatly facilitating compiler development. { They support certi cation of object code. By extending types to the ge- rated object code, it becomes possible for a code user to ensure the basic integrity of that code by checking its type consistency before execution. { They support optimized data representations and calling conventions, even in the presence of modularity. By passing types at compile-, link-, and even run-time, it is possible to avoid compromises of data representation imposed by untyped compilation techniques.


Assembly language Java data structure data structures programming programming language

Editors and affiliations

  • Robert┬áHarper
    • 1
  1. 1.Carnegie Mellon University School of Computer SciencePittsburghUSA

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2001
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-42196-2
  • Online ISBN 978-3-540-45332-1
  • Series Print ISSN 0302-9743
  • Buy this book on publisher's site
Industry Sectors
IT & Software
Consumer Packaged Goods
Finance, Business & Banking
Oil, Gas & Geosciences