Papers

Latest Publications

• Karl Crary. Explicit Contexts in LF. 2008 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.
  (pdf, twelf)

• Karl Crary and Robert Harper. Syntactic Logical Relations for Polymorphic and Recursive Types. Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, 2007.
  (pdf)

• Daniel K. Lee, Karl Crary, and Robert Harper. Mechanizing the Metatheory of Standard ML. 2006 Symposium on Principles of Programming Languages.
  (pdf, twelf)

• Karl Crary and Susmit Sarkar. Foundational Certified Code in a Metalogical Framework. ACM Transactions on Computational Logic, to appear.
  (pdf)

Other Recent Publications

• Karl Crary. Sound and Complete Elimination of Singleton Kinds. ACM Transactions on Computational Logic, 2007.
  (pdf)

• Susmit Sarkar, Brigitte Pientka, and Karl Crary. Small Proof Witnesses for LF. 2005 International Conference on Logic Programming.
  (pdf)

• Tom Murphy VII, Karl Crary, and Robert Harper. Distributed Control Flow with Classical Modal Logic. 2005 Computer Science Logic.
  (pdf)

• Karl Crary, Aleksey Kliger, and Frank Pfenning. A Monadic Analysis of Information Flow Security with Mutable State. Journal of Functional Programming: Special issue on Language-Based Security, March 2005.
  (pdf)

• Karl Crary. Logical Relations and a Case Study in Equivalence Checking. Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, 2005.

• Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning. A Symmetric Modal Lambda Calculus for Distributed Computing. 2004 Symposium on Logic in Computer Science.
  (pdf)
  Expanded Version. CMU Technical Report CMU-CS-04-105.
  (pdf)

• Karl Crary. Toward a Foundational Typed Assembly Language. 2003 Symposium on Principles of Programming Languages.
  (ps, pdf)
  Expanded Version. CMU Technical Report CMU-CS-02-196.
  (ps, pdf)

• Derek Dreyer, Karl Crary, and Robert Harper. A Type System for Higher-Order Modules. 2003 Symposium on Principles of Programming Languages.
  (ps, pdf)
  Expanded Version. CMU Technical Report CMU-CS-02-122R.
  (ps, pdf)

• Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning. A Type Theory for Memory Allocation and Data Layout. 2003 Symposium on Principles of Programming Languages.
  (ps, pdf)
  Expanded Version. CMU Technical Report CMU-CS-02-171.
  (ps, pdf)

• Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, and Perry Cheng. Typed Compilation of Recursive Datatypes. 2003 Workshop on Types in Language Design and Implementation.
  (ps, pdf)

• Joseph C. Vanderwaart and Karl Crary. A Typed Interface for Garbage Collection. 2003 Workshop on Types in Language Design and Implementation.
  (ps, pdf)

• Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, and Frank Pfenning. Trustless Grid Computing in ConCert. 2002 International Workshop on Grid Computing.
  (ps, pdf)

• Karl Crary and Joseph C. Vanderwaart. An Expressive, Scalable Type Theory for Certified Code. 2002 International Conference on Functional Programming.
  (ps, pdf)

• Joseph C. Vanderwaart and Karl Crary. A Simplified Account of the Metatheory of Linear LF. CMU Technical Report CMU-CS-01-154.
  (ps, pdf)
  Short Version. 2002 International Workshop on Logical Frameworks and Meta-Languages.
  (ps)

• Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in Type-Erasure Semantics. Journal of Functional Programming, November 2002.
  (ps)

• Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-Based Typed Assembly Language. Journal of Functional Programming, January 2002.
  (abstract, ps)

• Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, and Noel Walkington. Persistent Triangulations. Journal of Functional Programming, September 2001.
  (pdf)

• David Walker, Karl Crary, and Greg Morrisett. Typed Memory Management via Static Capabilities. ACM TOPLAS, July 2000.
  (abstract, ps, pdf)

• Michael Hicks, Stephanie Weirich, and Karl Crary. Safe and Flexible Dynamic Linking of Native Code. 2000 Workshop on Types in Compilation.
  (abstract, pdf)

• Karl Crary. Typed Compilation of Inclusive Subtyping. 2000 International Conference on Functional Programming.
  (abstract, ps)

• Karl Crary and Stephanie Weirich. Resource Bound Certification. 2000 Symposium on Principles of Programming Languages.
  (abstract, ps.gz, dvi)

• Karl Crary and Stephanie Weirich. Flexible Type Analysis. 1999 International Conference on Functional Programming.
  (abstract, ps.gz, dvi)

• Karl Crary. A Simple Proof Technique for Certain Parametricity Results. 1999 International Conference on Functional Programming.
  (abstract, ps.gz, dvi)

• Karl Crary and Greg Morrisett. Type Structure for Low-Level Programming Languages. 1999 International Colloquium on Automata, Languages, and Programming.
  (abstract, ps.gz, dvi)

• Karl Crary, Robert Harper, and Sidd Puri. What is a Recursive Module? 1999 Conference on Programming Language Design and Implementation.
  (abstract, ps.gz, dvi)

• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. ACM TOPLAS, May 1999.
  (abstract, ps)