| 2025 | FSCD | Substructural Parametricity. | C. B. Aberl, Karl Crary, Chris Martens, Frank Pfenning |
| 2018 | LICS | Strong Sums in Focused Logic. | Karl Crary |
| 2018 | PADL | Hygienic Source-Code Generation Using Functors - (Extended Abstract). | Karl Crary |
| 2017 | POPL | Modules, abstraction, and parametric polymorphism. | Karl Crary |
| 2015 | PLDI | Peer-to-peer affine commitment using bitcoin. | Karl Crary, Michael J. Sullivan |
| 2015 | POPL | A Calculus for Relaxed Memory. | Karl Crary, Michael J. Sullivan |
| 2010 | ICFP | Higher-order representation of substructural logics. | Karl Crary |
| 2007 | POPL | Towards a mechanized metatheory of standard ML. | Daniel K. Lee, Karl Crary, Robert Harper |
| 2005 | CSL | Distributed Control Flow with Classical Modal Logic. | Tom Murphy VII, Karl Crary, Robert Harper |
| 2005 | ICLP | Small Proof Witnesses for LF. | Susmit Sarkar, Brigitte Pientka, Karl Crary |
| 2004 | LICS | A Symmetric Modal Lambda Calculus for Distributed Computing. | Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning |
| 2003 | CADE | Foundational Certified Code in a Metalogical Framework. | Karl Crary, Susmit Sarkar |
| 2003 | POPL | Toward a foundational typed assembly language. | Karl Crary |
| 2003 | POPL | A type system for higher-order modules. | Derek Dreyer, Karl Crary, Robert Harper |
| 2003 | POPL | A type theory for memory allocation and data layout. | Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning |
| 2002 | ICFP | An expressive, scalable type theory for certified code. | Karl Crary, Joseph Vanderwaart |
| 2000 | ICFP | Typed compilation of inclusive subtyping. | Karl Crary |
| 2000 | POPL | Resource Bound Certification. | Karl Crary, Stephanie Weirich |
| 1999 | ICALP | Type Structure for Low-Level Programming Languages. | Karl Crary, J. Gregory Morrisett |
| 1999 | ICFP | A Simple Proof Technique for Certain Parametricity Results. | Karl Crary |
| 1999 | ICFP | Flexible Type Analysis. | Karl Crary, Stephanie Weirich |
| 1999 | PLDI | What is a Recursive Module? | Karl Crary, Robert Harper, Sidd Puri |
| 1999 | POPL | Typed Memory Management in a Calculus of Capabilities. | Karl Crary, David Walker, J. Gregory Morrisett |
| 1998 | CADE | Admissibility of Fixpoint Induction over Partial Types. | Karl Crary |
| 1998 | ICFP | Intensional Polymorphism in Type-Erasure Semantics. | Karl Crary, Stephanie Weirich, J. Gregory Morrisett |
| 1998 | POPL | From System F to Typed Assembly Language. | J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew |
| 1997 | ICFP | Foundations for the Implementation of Higher-Order Subtyping. | Karl Crary |