An expressive, scalable type theory for certified code

10 years 7 months ago
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. Categories and Subject Descriptors D.3 [Programming Languages]: Miscellaneous; F.3.1 [Theory of Computation]: Logics and Meanings of Programs. General Terms Languages, Security
Karl Crary, Joseph Vanderwaart
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2002
Where ICFP
Authors Karl Crary, Joseph Vanderwaart
Comments (0)