Karl Crary

Publication Activity (10 Years)

Years Active: 1997-2021
Publications (10 Years): 10

Top Topics

Code Generation

Piecewise Affine

Partial Deduction

Top Venues

Proc. ACM Program. Lang.

Publications

Karl Crary
Verifying the Hashgraph Consensus Algorithm. CoRR (2021)
Karl Crary
A focused solution to the avoidance problem. J. Funct. Program. 30 (2020)
Michael J. Sullivan, Karl Crary, Salil Joshi
Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrency. CoRR (2019)
Karl Crary
Fully abstract module compilation. Proc. ACM Program. Lang. 3 (POPL) (2019)
Karl Crary
Strong Sums in Focused Logic. LICS (2018)
Karl Crary
Hygienic Source-Code Generation Using Functors - (Extended Abstract). PADL (2018)
Brandon Bohrer, Karl Crary
TWAM: A Certifying Abstract Machine for Logic Programs. VSTTE (2018)
Karl Crary
Hygienic Source-Code Generation Using Functors. CoRR (2018)
Brandon Bohrer, Karl Crary
TWAM: A Certifying Abstract Machine for Logic Programs. CoRR (2018)
Karl Crary
Modules, abstraction, and parametric polymorphism. POPL (2017)
Karl Crary, Michael J. Sullivan
A Calculus for Relaxed Memory. POPL (2015)
Karl Crary, Michael J. Sullivan
Peer-to-peer affine commitment using bitcoin. PLDI (2015)
Karl Crary
Higher-order representation of substructural logics. ICFP (2010)
Karl Crary
A syntactic account of singleton types via hereditary substitution. LFMTP (2009)
Karl Crary
Explicit Contexts in LF (Extended Abstract). Electron. Notes Theor. Comput. Sci. 228 (2009)
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. Electron. Notes Theor. Comput. Sci. 172 (2007)
Karl Crary
Sound and complete elimination of singleton kinds. ACM Trans. Comput. Log. 8 (2) (2007)
Tom Murphy VII, Karl Crary, Robert Harper
Type-Safe Distributed Programming with ML5. TGC (2007)
Daniel K. Lee, Karl Crary, Robert Harper
Towards a mechanized metatheory of standard ML. POPL (2007)
Karl Crary, Robert Harper
Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight CoRR (2006)
David Swasey, Tom Murphy VII, Karl Crary, Robert Harper
A separate compilation extension to standard ML. ML (2006)
Karl Crary, Robert Harper
Higher-order abstract syntax: setting the record straight. SIGACT News 37 (3) (2006)
Susmit Sarkar, Brigitte Pientka, Karl Crary
Small Proof Witnesses for LF. ICLP (2005)
Joseph Vanderwaart, Karl Crary
Automated and certified conformance to responsiveness policies. TLDI (2005)
Tom Murphy VII, Karl Crary, Robert Harper
Distributed Control Flow with Classical Modal Logic. CSL (2005)
Karl Crary, Aleksey Kliger, Frank Pfenning
A monadic analysis of information flow security with mutable state. J. Funct. Program. 15 (2) (2005)
Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
A Symmetric Modal Lambda Calculus for Distributed Computing. LICS (2004)
J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker
Stack-based typed assembly language. J. Funct. Program. 13 (5) (2003)
Joseph Vanderwaart, Karl Crary
A typed interface for garbage collection. TLDI (2003)
Karl Crary
Toward a foundational typed assembly language. POPL (2003)
Karl Crary, Susmit Sarkar
Foundational Certified Code in a Metalogical Framework. CADE (2003)
Derek Dreyer, Karl Crary, Robert Harper
A type system for higher-order modules. POPL (2003)
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
Automated techniques for provably safe mobile code. Theor. Comput. Sci. 290 (2) (2003)
Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
Typed compilation of recursive datatypes. TLDI (2003)
Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
A type theory for memory allocation and data layout. POPL (2003)
Karl Crary, Stephanie Weirich, J. Gregory Morrisett
Intensional polymorphism in type-erasure semantics. J. Funct. Program. 12 (6) (2002)
J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker
Stack-based typed assembly language. J. Funct. Program. 12 (1) (2002)
Joseph Vanderwaart, Karl Crary
A Simplified Account of the Metatheory of Linear LF. Electron. Notes Theor. Comput. Sci. 70 (2) (2002)
Karl Crary, Joseph Vanderwaart
An expressive, scalable type theory for certified code. ICFP (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)
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) (2001)
David Walker, Karl Crary, J. Gregory Morrisett
Typed memory management via static capabilities. ACM Trans. Program. Lang. Syst. 22 (4) (2000)
Michael W. Hicks, Stephanie Weirich, Karl Crary
Safe and Flexible Dynamic Linking of Native Code. Types in Compilation (2000)
Karl Crary, Stephanie Weirich
Resource Bound Certification. POPL (2000)
Karl Crary
Sound and Complete Elimination of Singleton Kinds. Types in Compilation (2000)
Karl Crary
Typed compilation of inclusive subtyping. ICFP (2000)
J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew
From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21 (3) (1999)
Karl Crary, Robert Harper, Sidd Puri
What is a Recursive Module? PLDI (1999)
Karl Crary, David Walker, J. Gregory Morrisett
Typed Memory Management in a Calculus of Capabilities. POPL (1999)
Karl Crary
A Simple Proof Technique for Certain Parametricity Results. ICFP (1999)
Karl Crary, Stephanie Weirich
Flexible Type Analysis. ICFP (1999)
Karl Crary, J. Gregory Morrisett
Type Structure for Low-Level Programming Languages. ICALP (1999)
Karl Crary, Stephanie Weirich, J. Gregory Morrisett
Intensional Polymorphism in Type-Erasure Semantics. ICFP (1998)
J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker
Stack-Based Typed Assembly Language. Types in Compilation (1998)
J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew
From System F to Typed Assembly Language. POPL (1998)
Karl Crary
Programming language semantics in foundational type theory. PROCOMET (1998)
Karl Crary
Admissibility of Fixpoint Induction over Partial Types. CADE (1998)
Karl Crary
Foundations for the Implementation of Higher-Order Subtyping. ICFP (1997)