 Type Theory for Certified Code
started 5/5/2001; 4:43:22 AM - last post 5/5/2001; 4:43:22 AM
|
|
Ehud Lamm - Type Theory for Certified Code 
5/5/2001; 4:43:22 AM (reads: 1490, responses: 0)
|
|
| 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 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
Posted to theory by Ehud Lamm on 5/5/01; 4:43:36 AM
|
|
|
|
|
|