The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard's F_w kind level, this language is notable for containing singleton kinds and dependent product and function kinds. Previous work (CMU-CS-99-155) 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 the language. The particular use of intensional type analysis to handle arrays of unboxed floating point numbers is described. An extended calculus is also introduced which permits unlabelled singletons at higher kind, in order to allow for more compact program representation. The extended calculus is related to the restricted calculus via a transformation that eliminates the unlabelled singletons, and the decidability of the typechecking algorithms for both the original and extended calculus is shown.

47 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu