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

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

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

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.