Paper Announcement: An Expressive, Scalable Type Theory for Certified Code

To: types@cis.upenn.edu
Subject: Paper Announcement: An Expressive, Scalable Type Theory for Certified Code
From: Joseph Vanderwaart <Joseph_Vanderwaart@gs230.sp.cs.cmu.edu>
Date: Thu, 03 May 2001 13:33:42 -0400


We would like to announce the availability of the following paper at:
	http://www.cs.cmu.edu/~crary/papers/  or
	http://www.cs.cmu.edu/~joev/work.html

Comments or suggestions are always welcome.

-- Karl Crary and Joseph Vanderwaart


-------------------------
An Expressive, Scalable Type Theory for Certified Code
Karl Crary and Joseph C. Vanderwaart


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 provide
additional re-use with a framework for modular development of
operational semantics.  This framework allows independent type systems
and their operational semantics to be joined together, automatically
inheriting the type safety properties of those individual systems.