Computer Science Department
School of Computer Science, Carnegie Mellon University
An Expressive, Scalable Type Theory for Certified Code
Karl Crary, Joseph C. Vanderwaart
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.