 | 2009 |
|---|
| 45 |       | Karl Crary:
Explicit Contexts in LF (Extended Abstract).
Electr. Notes Theor. Comput. Sci. 228: 53-68 (2009) |
| 2008 |
|---|
| 44 | | Karl Crary,
Susmit Sarkar:
Foundational certified code in the Twelf metalogical framework.
ACM Trans. Comput. Log. 9(3): (2008) |
| 2007 |
|---|
| 43 | | Daniel K. Lee,
Karl Crary,
Robert Harper:
Towards a mechanized metatheory of standard ML.
POPL 2007: 173-184 |
| 42 | | Tom Murphy VII,
Karl Crary,
Robert Harper:
Type-Safe Distributed Programming with ML5.
TGC 2007: 108-123 |
| 41 | | Karl Crary:
Sound and complete elimination of singleton kinds.
ACM Trans. Comput. Log. 8(2): (2007) |
| 40 | | Karl Crary,
Robert Harper:
Syntactic Logical Relations for Polymorphic and Recursive Types.
Electr. Notes Theor. Comput. Sci. 172: 259-299 (2007) |
| 2006 |
|---|
| 39 | | David Swasey,
Tom Murphy VII,
Karl Crary,
Robert Harper:
A separate compilation extension to standard ML.
ML 2006: 32-42 |
| 38 | | Karl Crary,
Robert Harper:
Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight
CoRR abs/cs/0607141: (2006) |
| 37 | | Karl Crary,
Robert Harper:
Higher-order abstract syntax: setting the record straight.
SIGACT News 37(3): 93-96 (2006) |
| 2005 |
|---|
| 36 | | Tom Murphy VII,
Karl Crary,
Robert Harper:
Distributed Control Flow with Classical Modal Logic.
CSL 2005: 51-69 |
| 35 | | Susmit Sarkar,
Brigitte Pientka,
Karl Crary:
Small Proof Witnesses for LF.
ICLP 2005: 387-401 |
| 34 | | Joseph Vanderwaart,
Karl Crary:
Automated and certified conformance to responsiveness policies.
TLDI 2005: 79-90 |
| 33 | | Karl Crary,
Aleksey Kliger,
Frank Pfenning:
A monadic analysis of information flow security with mutable state.
J. Funct. Program. 15(2): 249-291 (2005) |
| 2004 |
|---|
| 32 | | Tom Murphy VII,
Karl Crary,
Robert Harper,
Frank Pfenning:
A Symmetric Modal Lambda Calculus for Distributed Computing.
LICS 2004: 286-295 |
| 2003 |
|---|
| 31 | | Karl Crary,
Susmit Sarkar:
Foundational Certified Code in a Metalogical Framework.
CADE 2003: 106-120 |
| 30 | | Leaf Petersen,
Robert Harper,
Karl Crary,
Frank Pfenning:
A type theory for memory allocation and data layout.
POPL 2003: 172-184 |
| 29 | | Karl Crary:
Toward a foundational typed assembly language.
POPL 2003: 198-212 |
| 28 | | Derek Dreyer,
Karl Crary,
Robert Harper:
A type system for higher-order modules.
POPL 2003: 236-249 |
| 27 | | Joseph Vanderwaart,
Karl Crary:
A typed interface for garbage collection.
TLDI 2003: 109-122 |
| 26 | | Joseph Vanderwaart,
Derek Dreyer,
Leaf Petersen,
Karl Crary,
Robert Harper,
Perry Cheng:
Typed compilation of recursive datatypes.
TLDI 2003: 98-108 |
| 25 | | J. Gregory Morrisett,
Karl Crary,
Neal Glew,
David Walker:
Stack-based typed assembly language.
J. Funct. Program. 13(5): 957-959 (2003) |
| 24 |  | 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) |
| 2002 |
|---|
| 23 | | 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 |
| 22 | | Karl Crary,
Joseph Vanderwaart:
An expressive, scalable type theory for certified code.
ICFP 2002: 191-205 |
| 21 | | Joseph Vanderwaart,
Karl Crary:
A Simplified Account of the Metatheory of Linear LF.
Electr. Notes Theor. Comput. Sci. 70(2): (2002) |
| 20 | | J. Gregory Morrisett,
Karl Crary,
Neal Glew,
David Walker:
Stack-based typed assembly language.
J. Funct. Program. 12(1): 3-88 (2002) |
| 19 | | Karl Crary,
Stephanie Weirich,
J. Gregory Morrisett:
Intensional polymorphism in type-erasure semantics.
J. Funct. Program. 12(6): 567-600 (2002) |
| 2001 |
|---|
| 18 | | 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) |
| 2000 |
|---|
| 17 | | Karl Crary:
Typed compilation of inclusive subtyping.
ICFP 2000: 68-81 |
| 16 | | Karl Crary,
Stephanie Weirich:
Resource Bound Certification.
POPL 2000: 184-198 |
| 15 | | Karl Crary:
Sound and Complete Elimination of Singleton Kinds.
Types in Compilation 2000: 1-26 |
| 14 | | Michael W. Hicks,
Stephanie Weirich,
Karl Crary:
Safe and Flexible Dynamic Linking of Native Code.
Types in Compilation 2000: 147-176 |
| 13 | | David Walker,
Karl Crary,
J. Gregory Morrisett:
Typed memory management via static capabilities.
ACM Trans. Program. Lang. Syst. 22(4): 701-771 (2000) |
| 1999 |
|---|
| 12 | | Karl Crary,
J. Gregory Morrisett:
Type Structure for Low-Level Programming Languages.
ICALP 1999: 40-54 |
| 11 | | Karl Crary,
Stephanie Weirich:
Flexible Type Analysis.
ICFP 1999: 233-248 |
| 10 | | Karl Crary:
A Simple Proof Technique for Certain Parametricity Results.
ICFP 1999: 82-89 |
| 9 | | Karl Crary,
Robert Harper,
Sidd Puri:
What is a Recursive Module?
PLDI 1999: 50-63 |
| 8 | | Karl Crary,
David Walker,
J. Gregory Morrisett:
Typed Memory Management in a Calculus of Capabilities.
POPL 1999: 262-275 |
| 7 | | 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) |
| 1998 |
|---|
| 6 | | Karl Crary:
Admissibility of Fixpoint Induction over Partial Types.
CADE 1998: 270-285 |
| 5 | | Karl Crary,
Stephanie Weirich,
J. Gregory Morrisett:
Intensional Polymorphism in Type-Erasure Semantics.
ICFP 1998: 301-312 |
| 4 | | J. Gregory Morrisett,
David Walker,
Karl Crary,
Neal Glew:
From System F to Typed Assembly Language.
POPL 1998: 85-97 |
| 3 | | Karl Crary:
Programming language semantics in foundational type theory.
PROCOMET 1998: 107-125 |
| 2 | | J. Gregory Morrisett,
Karl Crary,
Neal Glew,
David Walker:
Stack-Based Typed Assembly Language.
Types in Compilation 1998: 28-52 |
| 1997 |
|---|
| 1 | | Karl Crary:
Foundations for the Implementation of Higher-Order Subtyping.
ICFP 1997: 125-135 |
