CMU-CS-01-113 Computer Science Department School of Computer Science, Carnegie Mellon University
An Expressive, Scalable Type Theory for Certified Code Karl Crary, Joseph C. Vanderwaart May 2001
CMU-CS-01-113.ps
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. 27 pages
| |
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |