| Implementing the TILT Internal Language |
DEC 2000 |
47 pages |
| Authors:
Leaf Petersen; Perry Cheng; Robert Harper; Chris Stone; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
 | The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard's F omega. At the kind level, this language is notable for containing singleton kinds and dependent product and function kinds. Previous work SH99 established the decidability of type equivalence for this language. This paper presents a typechecking algorithm for the full TILT internal language and discusses some of the more interesting features of ... |
|
| Transparent and Opaque Interpretations of Datatypes |
NOV 1998 |
8 pages |
| Authors:
Karl Crary; Robert Harper; Perry Cheng; Leaf Petersen; Chris Stone; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Standard ML employs an opaque (or generative) interpretation of datatype specifications, in which every datatype specification provides a new, abstract type that is different from any other type, including other identically specified datatypes. An alternative interpretation is the transparent one, in which a datatype specification exposes the underlying recursive type implementation of the datatype. It is commonly believed that the transparent interpretation is strictly more permissive than the opaque interpretation; ... |
|
| A Type-Theoretic Account of Standard ML 1996 (Version 1) |
10 MAY 96 |
|
| Authors:
Chris Stone; Robert Harper; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
 | A type-theoretic definition of a variant of the Standard ML (Revised 1996) programming language is given. The definition consists of a syntax- directed translation of SML96 programs into a typed intermediate language. The intermediate language is an explicitly-typed lambda-calculus with product, sum, recursive, and module types. The translation performs type reconstruction, handles identifier scope resolution, enforces static well-formedness conditions, and expands high-level constructs (such as pattern matching and signature matching) ... |
|
| TIL: A Type-Directed Optimizing Compiler for ML |
29 FEB 96 |
|
| Authors:
David Tarditi; Chris Stone; Greg Morrisett; Robert Harper; Perry Cheng; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
| We describe a new compiler for Standard ML called TIL, that is based on four technologies: intensional polymorphism, tag-free garbage collection, conventional functional language optimization and loop optimization. We use intensional polymorphism and tag-free garbage collection to provide specialized representations, even though SML is a polymorphic language. We use conventional functional language optimization to reduce the cost of intensional polymorphism, and loop optimization to generate good code for recursive functions. ... |
|
Reports by Author
