Karl Crary

Karl Crary: Higher-order representation of substructural logics. ICFP 2010: 131-142

Karl Crary, Marino Miculan (Eds.): Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. EPTCS 34, 2010

Karl Crary: Explicit Contexts in LF (Extended Abstract). Electr. Notes Theor. Comput. Sci. 228: 53-68 (2009)

Karl Crary: A syntactic account of singleton types via hereditary substitution. LFMTP 2009: 21-29

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

Karl Crary, Robert Harper: Syntactic Logical Relations for Polymorphic and Recursive Types. Electr. Notes Theor. Comput. Sci. 172: 259-299 (2007)

Karl Crary: Sound and complete elimination of singleton kinds. ACM Trans. Comput. Log. 8(2) (2007)

Daniel K. Lee, Karl Crary, Robert Harper: Towards a mechanized metatheory of standard ML. POPL 2007: 173-184

Tom Murphy VII, Karl Crary, Robert Harper: Type-Safe Distributed Programming with ML5. TGC 2007: 108-123

Karl Crary, Robert Harper: Higher-order abstract syntax: setting the record straight. SIGACT News 37(3): 93-96 (2006)

David Swasey, Tom Murphy VII, Karl Crary, Robert Harper: A separate compilation extension to standard ML. ML 2006: 32-42

Karl Crary, Robert Harper: Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight. CoRR abs/cs/0607141 (2006)

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

Tom Murphy VII, Karl Crary, Robert Harper: Distributed Control Flow with Classical Modal Logic. CSL 2005: 51-69

Susmit Sarkar, Brigitte Pientka, Karl Crary: Small Proof Witnesses for LF. ICLP 2005: 387-401

Joseph Vanderwaart, Karl Crary: Automated and certified conformance to responsiveness policies. TLDI 2005: 79-90

Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning: A Symmetric Modal Lambda Calculus for Distributed Computing. LICS 2004: 286-295

J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker: Stack-based typed assembly language. J. Funct. Program. 13(5): 957-959 (2003)

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning: Automated techniques for provably safe mobile code. Theor. Comput. Sci. 290(2): 1175-1199 (2003)

Karl Crary, Susmit Sarkar: Foundational Certified Code in a Metalogical Framework. CADE 2003: 106-120

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning: A type theory for memory allocation and data layout. POPL 2003: 172-184

Karl Crary: Toward a foundational typed assembly language. POPL 2003: 198-212

Derek Dreyer, Karl Crary, Robert Harper: A type system for higher-order modules. POPL 2003: 236-249

Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng: Typed compilation of recursive datatypes. TLDI 2003: 98-108

Joseph Vanderwaart, Karl Crary: A typed interface for garbage collection. TLDI 2003: 109-122

Joseph Vanderwaart, Karl Crary: A Simplified Account of the Metatheory of Linear LF. Electr. Notes Theor. Comput. Sci. 70(2): 11-28 (2002)

J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker: Stack-based typed assembly language. J. Funct. Program. 12(1): 3-88 (2002)

Karl Crary, Stephanie Weirich, J. Gregory Morrisett: Intensional polymorphism in type-erasure semantics. J. Funct. Program. 12(6): 567-600 (2002)

Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning: Trustless Grid Computing in ConCert. GRID 2002: 112-125

Karl Crary, Joseph Vanderwaart: An expressive, scalable type theory for certified code. ICFP 2002: 191-205

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

David Walker, Karl Crary, J. Gregory Morrisett: Typed memory management via static capabilities. ACM Trans. Program. Lang. Syst. 22(4): 701-771 (2000)

Karl Crary: Typed compilation of inclusive subtyping. ICFP 2000: 68-81

Karl Crary, Stephanie Weirich: Resource Bound Certification. POPL 2000: 184-198

Karl Crary: Sound and Complete Elimination of Singleton Kinds. Types in Compilation 2000: 1-26

Michael W. Hicks, Stephanie Weirich, Karl Crary: Safe and Flexible Dynamic Linking of Native Code. Types in Compilation 2000: 147-176

J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew: From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3): 527-568 (1999)

Karl Crary, J. Gregory Morrisett: Type Structure for Low-Level Programming Languages. ICALP 1999: 40-54

Karl Crary: A Simple Proof Technique for Certain Parametricity Results. ICFP 1999: 82-89

Karl Crary, Stephanie Weirich: Flexible Type Analysis. ICFP 1999: 233-248

Karl Crary, Robert Harper, Sidd Puri: What is a Recursive Module? PLDI 1999: 50-63

Karl Crary, David Walker, J. Gregory Morrisett: Typed Memory Management in a Calculus of Capabilities. POPL 1999: 262-275

Karl Crary: Admissibility of Fixpoint Induction over Partial Types. CADE 1998: 270-285

Karl Crary, Stephanie Weirich, J. Gregory Morrisett: Intensional Polymorphism in Type-Erasure Semantics. ICFP 1998: 301-312

J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew: From System F to Typed Assembly Language. POPL 1998: 85-97

Karl Crary: Programming language semantics in foundational type theory. PROCOMET 1998: 107-125

J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker: Stack-Based Typed Assembly Language. Types in Compilation 1998: 28-52

Karl Crary: Foundations for the Implementation of Higher-Order Subtyping. ICFP 1997: 125-135