Papers

Latest Publications

• Karl Crary. Verifying the Hashgraph Consensus Algorithm. 2021.
  (pdf, coq)

• Karl Crary. A Focused Solution to the Avoidance Problem. Journal of Functional Programming, essays in honor of Robert Harper, 2020.
  (pdf, coq)

• Karl Crary. Fully Abstract Module Compilation. 2019 Symposium on Principles of Programming Languages.
  (pdf, coq)

Other Recent Publications

• Karl Crary. Correctness proof for the Hashgraph Consensus algorithm, formalized in Coq. 2018. (Unpublished; experience paper forthcoming.)
  (coq)

• Karl Crary. Strong Sums in Focused Logic. 2018 Symposium on Logic in Computer Science.
  (pdf, coq)

• Brandon Bohrer and Karl Crary. TWAM: A Certifying Abstract Machine for Logic Programs. 2018 Working Conference on Verified Software: Theories, Tools, and Experiments.
  (pdf)

• Karl Crary. Hygienic Source-Code Generation Using Functors. 2018 International Symposium on Practical Aspects of Declarative Languages.
  (pdf, project page)

• Michael J. Sullivan, Karl Crary, and Salil Joshi. Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrency. 2017.
  (pdf)

• Karl Crary. Modules, Abstraction, and Parametric Polymorphism. 2017 Symposium on Principles of Programming Languages.
  (pdf, coq)

• Karl Crary and Michael J. Sullivan. Peer-to-Peer Affine Commitment using Bitcoin. 2015 Conference on Programming Language Design and Implementation.
  (pdf)

• Karl Crary and Michael J. Sullivan. A Calculus for Relaxed Memory. 2015 Symposium on Principles of Programming Languages.
  (pdf, coq)

• Chris Martens and Karl Crary LF in LF: Mechanizing the Metatheories of LF in Twelf. 2012 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.
  (pdf)

• Karl Crary. Higher-order Representation of Substructural Logics. 2010 International Conference on Functional Programming.
  (pdf, twelf)

• Karl Crary and Robert Harper. Mechanized Definition of Standard ML (alpha release). 2009.
  (twelf)

• Karl Crary. A Simple Proof of Call-by-Value Standardization. CMU Technical Report CMU-CS-09-137, 2009.
  (pdf, twelf)

• Karl Crary. A Syntactic Account of Singleton Types via Hereditary Substitution. 2009 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.
  (pdf, twelf)

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

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

• 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. Towards a Mechanized Metatheory of Standard ML. 2007 Symposium on Principles of Programming Languages.
  (pdf, twelf)

• Tom Murphy VII, Karl Crary, and Robert Harper. Type-safe Distributed Programming with ML5. Symposium on Trustworthy Global Computing, 2007.
  (pdf)

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

• Tom Murphy VII, Daniel Spoonhower, Chris Casinghino, Daniel R. Licata, Karl Crary, and Robert Harper. The Cult of the Bound Variable: The 9th Annual ICFP Programming Contest. CMU Technical Report CMU-CS-06-163, 2006.
  (pdf)

• David Swasey, Tom Murphy VII, Karl Crary, and Robert Harper. A Separate Compilation Extension to Standard ML. Workshop on ML, 2006.
  (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)

• Joseph C. Vanderwaart and Karl Crary. Foundational Typed Assembly Language for Grid Computing. CMU Technical Report CMU-CS-04-104, 2004.
  (pdf)

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

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

• Joseph C. Vanderwaart and Karl Crary. A Typed Interface for Garbage Collection. 2003 Workshop on Types in Language Design and Implementation.
  (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.
  (pdf)

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

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

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

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

• 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.
  (pdf)

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

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

• Karl Crary and Stephanie Weirich. Resource Bound Certification. 2000 Symposium on Principles of Programming Languages.
  (pdf)

• Karl Crary and Stephanie Weirich. Flexible Type Analysis. 1999 International Conference on Functional Programming.
  (pdf)

• Karl Crary. A Simple Proof Technique for Certain Parametricity Results. 1999 International Conference on Functional Programming.
  (pdf)

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

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

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