CMU-CS-00-153Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-00-153
Christopher Allan Stone August 2000 Ph.D. Thesis
CMU-CS-00-153.ps
Keywords: Singleton Kinds, Singleton Types, type theory,
typechecking, typed compilation lambda calculus
However, the decidability of typechecking in the presence of singletons is not obvious. In order to typecheck a term, one must be able to determine whether two type constructors are provably equivalent. But in the presence of singleton kinds, the equivalence of type constructors depends both on the typing context in which they are compared and on the kind at which they are compared. In this dissertation I present MIL-0, a lambda calculus with singletons that is based upon the representation used by the TILT compiler. I prove important properties of this language, including type soundness and decidability of typechecking. The main technical result is decidability of equivalence for well-formed type constructors. Inspired by Coquand's result for type theory, I prove decidability of constructor equivalence for MIL-0 by exhibiting a novel -- though slightly inefficient -- type-directed comparison algorithm. The correctness of this algorithm is proved using an interesting variant of Kripke-style logical relations: unary relations are indexed by a single possible world (in our case, a typing context), but binary relations are indexed by two worlds. Using this result I can then show the correctness of a natural, practical algorithm used by the TILT compiler. 177 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |