Karl Crary

According to our database, Karl Crary authored at least 54 papers between 1997 and 2021.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2021

Verifying the Hashgraph Consensus Algorithm.

Karl Crary

CoRR, 2021

2020

A focused solution to the avoidance problem.

Karl Crary

J. Funct. Program., 2020

2019

Fully abstract module compilation.

Karl Crary

Proc. ACM Program. Lang., 2019

Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrency.

Michael J. Sullivan, Karl Crary, Salil Joshi

CoRR, 2019

2018

Hygienic Source-Code Generation Using Functors.

Karl Crary

CoRR, 2018

TWAM: A Certifying Abstract Machine for Logic Programs.

Rose Bohrer, Karl Crary

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Hygienic Source-Code Generation Using Functors - (Extended Abstract).

Karl Crary

Proceedings of the Practical Aspects of Declarative Languages, 2018

Strong Sums in Focused Logic.

Karl Crary

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

Modules, abstraction, and parametric polymorphism.

Karl Crary

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2015

A Calculus for Relaxed Memory.

Karl Crary, Michael J. Sullivan

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Peer-to-peer affine commitment using bitcoin.

Karl Crary, Michael J. Sullivan

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2010

Higher-order representation of substructural logics.

Karl Crary

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

2009

A syntactic account of singleton types via hereditary substitution.

Karl Crary

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2009

2008

Foundational certified code in the Twelf metalogical framework.

Karl Crary, Susmit Sarkar

ACM Trans. Comput. Log., 2008

Explicit Contexts in LF (Extended Abstract).

Karl Crary

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

2007

Sound and complete elimination of singleton kinds.

Karl Crary

ACM Trans. Comput. Log., 2007

Syntactic Logical Relations for Polymorphic and Recursive Types.

Karl Crary, Robert Harper

Proceedings of the Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, 2007

Type-Safe Distributed Programming with ML5.

Tom Murphy VII, Karl Crary, Robert Harper

Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Towards a mechanized metatheory of standard ML.

Daniel K. Lee, Karl Crary, Robert Harper

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

2006

Higher-order abstract syntax: setting the record straight.

Karl Crary, Robert Harper

SIGACT News, 2006

Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight

Karl Crary, Robert Harper

CoRR, 2006

A separate compilation extension to standard ML.

David Swasey, Tom Murphy VII, Karl Crary, Robert Harper

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

2005

A monadic analysis of information flow security with mutable state.

Karl Crary, Aleksey Kliger, Frank Pfenning

J. Funct. Program., 2005

Automated and certified conformance to responsiveness policies.

Joseph Vanderwaart, Karl Crary

Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

Small Proof Witnesses for LF.

Susmit Sarkar, Brigitte Pientka, Karl Crary

Proceedings of the Logic Programming, 21st International Conference, 2005

Distributed Control Flow with Classical Modal Logic.

Tom Murphy VII, Karl Crary, Robert Harper

Proceedings of the Computer Science Logic, 19th International Workshop, 2005

2004

A Symmetric Modal Lambda Calculus for Distributed Computing.

Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning

Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

2003

Automated techniques for provably safe mobile code.

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

Theor. Comput. Sci., 2003

Typed compilation of recursive datatypes.

Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng

Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2003

A typed interface for garbage collection.

Joseph Vanderwaart, Karl Crary

Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2003

A type theory for memory allocation and data layout.

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

A type system for higher-order modules.

Derek Dreyer, Karl Crary, Robert Harper

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

Toward a foundational typed assembly language.

Karl Crary

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

Foundational Certified Code in a Metalogical Framework.

Karl Crary, Susmit Sarkar

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Stack-based typed assembly language.

J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker

J. Funct. Program., 2002

Intensional polymorphism in type-erasure semantics.

Karl Crary, Stephanie Weirich, J. Gregory Morrisett

J. Funct. Program., 2002

A Simplified Account of the Metatheory of Linear LF.

Joseph Vanderwaart, Karl Crary

Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 2002

An expressive, scalable type theory for certified code.

Karl Crary, Joseph Vanderwaart

Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), 2002

Trustless Grid Computing in ConCert.

Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning

Proceedings of the Grid Computing, 2002

2001

Persistent triangulations Journal of Functional Programming.

Guy E. Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary L. Miller, Noel Walkington

J. Funct. Program., 2001

2000

Typed memory management via static capabilities.

David Walker, Karl Crary, J. Gregory Morrisett

ACM Trans. Program. Lang. Syst., 2000

Safe and Flexible Dynamic Linking of Native Code.

Michael W. Hicks, Stephanie Weirich, Karl Crary

Proceedings of the Types in Compilation, Third International Workshop, 2000

Resource Bound Certification.

Karl Crary, Stephanie Weirich

Proceedings of the POPL 2000, 2000

Typed compilation of inclusive subtyping.

Karl Crary

Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

1999

From system F to typed assembly language.

J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew

ACM Trans. Program. Lang. Syst., 1999

Typed Memory Management in a Calculus of Capabilities.

Karl Crary, David Walker, J. Gregory Morrisett

Proceedings of the POPL '99, 1999

What is a Recursive Module?

Karl Crary, Robert Harper, Sidd Puri

Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 1999

Flexible Type Analysis.

Karl Crary, Stephanie Weirich

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

A Simple Proof Technique for Certain Parametricity Results.

Karl Crary

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Type Structure for Low-Level Programming Languages.

Karl Crary, J. Gregory Morrisett

Proceedings of the Automata, 1999

1998

Type-Theoretic Methodology for Practical Programming Languages.

Karl Crary

PhD thesis, 1998

Programming language semantics in foundational type theory.

Karl Crary

Proceedings of the Programming Concepts and Methods, 1998

Admissibility of Fixpoint Induction over Partial Types.

Karl Crary

Proceedings of the Automated Deduction, 1998

1997

Foundations for the Implementation of Higher-Order Subtyping.

Karl Crary

Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997