An Expressive, Scalable Type Theory for Certified Code

We present the type theory LTT, intended to form a basis for typed target languages, providing an internal notion of logical proposition and proof. The inclusion of explicit proofs allows the type system to guarantee properties that would otherwise be incompatible with decidable type checking. LTT also provides linear facilities for tracking ephemeral properties that hold only for certain program states. Our type theory allows for re-use of typechecking software by casting a variety of type systems within a single language. We illustrate our methodology of representation by means of two examples, one functional and one stateful, and describe the associated operational semantics and proofs of type safety