Neal Glew's Dissertation

The official Cornell dissertation format is not very tree friendly.  So I have prepared a version of my dissertation that has a more resonable format but the same content.  If you really want the official format you can obtain it from Cornell University, through UMI, or by contacting me.  You should reference this version by section number not by page number.

Neal Glew.  Low-Level Type Systems for Modularity and Object-Oriented Constructs.  PhD dissertation, Cornell University, January 2000 (dvi, pdf, ps.gz).

Abstract

Typed Assembly Language (TAL) is a formal language for an idealised machine augmented with type annotations, typing rules, and a memory allocation primitive.  TAL's type system is sound; that is, well typed TAL programs do not commit run-time type errors during execution. This guarantee can be used to debug type-directed compilers and to build more general security properties in an extensible system. This dissertation presents a basic version of TAL and extensions to support the compilation of modules and object-oriented languages. First, it describes a modular version of TAL that consists of typed object files, linking operations, and link compatibility conditions. Together these features provide for type-sound separate compilation and substantially extend previous work on linking. Second, it shows how to use a new formulation of self quantifiers to compile an efficient implementation of a single-inheritance class-based object-oriented language into TAL.  Third, it presents a new type constructor called a tag type, and shows how to use them to compile downcasting and exceptions into TAL.

BibTeX Entry

@string{cucs-address="4130 Upson Hall, Ithaca, NY 14853-7501, USA"}
@PhdThesis{glew-thesis,
  author =       {Neal Glew},
  title =        {Low-Level Type Systems for Modularity and
                  Object-Oriented Constructs},
  school =       {Cornell University},
  year =         2000,
  address =      cucs-address,
  month =        jan
}