Computer Science Department
School of Computer Science, Carnegie Mellon University
Implementing the TILT Internal Language
Leaf Petersen, Perry Cheng, Robert Harper, Chris Stone
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.