Implementing the TILT Internal Language

Abstract

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 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 unlabeled 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 unlabeled singletons, and the decidability of the typechecking algorithms for both the original and extended calculus is shown.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 2000
Accession Number
ADA387219

Entities

People

  • Chris Stone
  • Leaf Petersen
  • Perry Cheng
  • Robert Harper

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Calculus
  • Compilers
  • Computer Programming
  • Computer Science
  • Computers
  • Elimination
  • Judgment
  • Language
  • Machine Languages
  • Machine Learning
  • Optimization
  • Plastic Explosives
  • Programming Languages
  • Semantics
  • Standardization
  • Standards

Readers

  • Computational Linguistics