COMPUTER SCIENCE TECHNICAL REPORT ABSTRACTS

Source: http://reports-archive.adm.cs.cmu.edu/anon/2001/abstracts/01-113.html Parent: https://www.cs.cmu.edu/~fox/publications.html


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

CMU-CS-01-113 Computer Science Department School of Computer Science, Carnegie Mellon University --- CMU-CS-01-113 An Expressive, Scalable Type Theory for Certified Code Karl Crary, Joseph C. Vanderwaart May 2001 CMU-CS-01-113.ps CMU-CS-01-113.pdf Keywords: Certified code, logical frameworks, type theory, linear logic 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. 27 pages

--- Return to: SCS Technical Report Collection School of Computer Science homepage This page maintained by reports@cs.cmu.edu