Foundations for the Implementation of Higher-Order Subtyping. - Karl Crary (ICFP, 1997)

Admissibility of Fixpoint Induction over Partial Types. - Karl Crary (CADE, 1998)

Programming language semantics in foundational type theory. - Karl Crary (PROCOMET, 1998)

Type-Theoretic Methodology for Practical Programming Languages. - Karl Crary (1998)

Type Structure for Low-Level Programming Languages. - Karl Crary; J. Gregory Morrisett (ICALP, 1999)

A Simple Proof Technique for Certain Parametricity Results. - Karl Crary (ICFP, 1999)

Flexible Type Analysis. - Karl Crary; Stephanie Weirich (ICFP, 1999)

What is a Recursive Module? - Karl Crary; Robert Harper 001; Sidd Puri (PLDI, 1999)

Typed Memory Management in a Calculus of Capabilities. - Karl Crary; David Walker 001; J. Gregory Morrisett (POPL, 1999)

From system F to typed assembly language. - J. Gregory Morrisett; David Walker 001; Karl Crary; Neal Glew (ACM Trans. Program. Lang. Syst., 1999)

Typed compilation of inclusive subtyping. - Karl Crary (ICFP, 2000)

Resource Bound Certification. - Karl Crary; Stephanie Weirich (POPL, 2000)

Safe and Flexible Dynamic Linking of Native Code. - Michael W. Hicks; Stephanie Weirich; Karl Crary (Types in Compilation, 2000)

Typed memory management via static capabilities. - David Walker 001; Karl Crary; J. Gregory Morrisett (ACM Trans. Program. Lang. Syst., 2000)

Persistent triangulations Journal of Functional Programming. - Guy E. Blelloch; Hal Burch; Karl Crary; Robert Harper 001; Gary L. Miller; Noel Walkington (J. Funct. Program., 2001)

Trustless Grid Computing in ConCert. - Bor-Yuh Evan Chang; Karl Crary; Margaret DeLap; Robert Harper 001; Jason Liszka; Tom Murphy VII; Frank Pfenning (GRID, 2002)

An expressive, scalable type theory for certified code. - Karl Crary; Joseph Vanderwaart (ICFP, 2002)

A Simplified Account of the Metatheory of Linear LF. - Joseph Vanderwaart; Karl Crary (LFM, 2002)

Intensional polymorphism in type-erasure semantics. - Karl Crary; Stephanie Weirich; J. Gregory Morrisett (J. Funct. Program., 2002)

Foundational Certified Code in a Metalogical Framework. - Karl Crary; Susmit Sarkar (CADE, 2003)

Toward a foundational typed assembly language. - Karl Crary (POPL, 2003)

A type system for higher-order modules. - Derek Dreyer; Karl Crary; Robert Harper 001 (POPL, 2003)

A type theory for memory allocation and data layout. - Leaf Petersen; Robert Harper 001; Karl Crary; Frank Pfenning (POPL, 2003)

A typed interface for garbage collection. - Joseph Vanderwaart; Karl Crary (TLDI, 2003)

Typed compilation of recursive datatypes. - Joseph Vanderwaart; Derek Dreyer; Leaf Petersen; Karl Crary; Robert Harper 001; Perry Cheng (TLDI, 2003)

Stack-based typed assembly language. - J. Gregory Morrisett; Karl Crary; Neal Glew; David Walker 001 (J. Funct. Program., 2003)

Automated techniques for provably safe mobile code. - Christopher Colby; Karl Crary; Robert Harper 001; Peter Lee 001; Frank Pfenning (Theor. Comput. Sci., 2003)

A Symmetric Modal Lambda Calculus for Distributed Computing. - Tom Murphy VII; Karl Crary; Robert Harper 001; Frank Pfenning (LICS, 2004)

Distributed Control Flow with Classical Modal Logic. - Tom Murphy VII; Karl Crary; Robert Harper 001 (CSL, 2005)

Small Proof Witnesses for LF. - Susmit Sarkar; Brigitte Pientka; Karl Crary (ICLP, 2005)

Automated and certified conformance to responsiveness policies. - Joseph Vanderwaart; Karl Crary (TLDI, 2005)

A monadic analysis of information flow security with mutable state. - Karl Crary; Aleksey Kliger; Frank Pfenning (J. Funct. Program., 2005)

A separate compilation extension to standard ML. - David Swasey; Tom Murphy VII; Karl Crary; Robert Harper 001 (ML, 2006)

Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight - Karl Crary; Robert Harper 001 (CoRR, 2006)

Higher-order abstract syntax: setting the record straight. - Karl Crary; Robert Harper 001 (SIGACT News, 2006)

Towards a mechanized metatheory of standard ML. - Daniel K. Lee; Karl Crary; Robert Harper 001 (POPL, 2007)

Type-Safe Distributed Programming with ML5. - Tom Murphy VII; Karl Crary; Robert Harper 001 (TGC, 2007)

Syntactic Logical Relations for Polymorphic and Recursive Types. - Karl Crary; Robert Harper 001 (Computation, Meaning, and Logic, 2007)

Sound and complete elimination of singleton kinds. - Karl Crary (ACM Trans. Comput. Log., 2007)

Explicit Contexts in LF (Extended Abstract). - Karl Crary (LFMTP@LICS, 2008)

Foundational certified code in the Twelf metalogical framework. - Karl Crary; Susmit Sarkar (ACM Trans. Comput. Log., 2008)

A syntactic account of singleton types via hereditary substitution. - Karl Crary (LFMTP, 2009)

Higher-order representation of substructural logics. - Karl Crary (ICFP, 2010)

Peer-to-peer affine commitment using bitcoin. - Karl Crary; Michael J. Sullivan (PLDI, 2015)

A Calculus for Relaxed Memory. - Karl Crary; Michael J. Sullivan (POPL, 2015)

Modules, abstraction, and parametric polymorphism. - Karl Crary (POPL, 2017)

Strong Sums in Focused Logic. - Karl Crary (LICS, 2018)

Hygienic Source-Code Generation Using Functors - (Extended Abstract). - Karl Crary (PADL, 2018)

TWAM: A Certifying Abstract Machine for Logic Programs. - Rose Bohrer; Karl Crary (VSTTE, 2018)

Hygienic Source-Code Generation Using Functors. - Karl Crary (CoRR, 2018)

Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrency. - Michael J. Sullivan; Karl Crary; Salil Joshi 004 (CoRR, 2019)

Fully abstract module compilation. - Karl Crary (Proc. ACM Program. Lang., 2019)

A focused solution to the avoidance problem. - Karl Crary (J. Funct. Program., 2020)

Verifying the Hashgraph Consensus Algorithm. - Karl Crary (CoRR, 2021)

Substructural Parametricity. - C. B. Aberlé; Karl Crary; Chris Martens 001; Frank Pfenning (FSCD, 2025)