Travelled to:1 × Canada
1 × Czech Republic
1 × Finland
1 × Germany
1 × India
1 × Spain
1 × The Netherlands
1 × United Kingdom
10 × USA
2 × France
Collaborated with:∅ R.Harper J.G.Morrisett S.Weirich M.J.Sullivan S.Sarkar T.M.VII D.Walker F.Pfenning J.Vanderwaart D.K.Lee B.Pientka D.Dreyer S.Puri L.Petersen N.Glew
Talks about:type (11) modul (4) calculus (3) languag (3) foundat (3) memori (3) higher (3) order (3) polymorph (2) distribut (2)
Person: Karl Crary
DBLP: Crary:Karl
Contributed to:
2015
2015
20102007
2005
2005
2004
20032003200220002000
1999199919991999199819981998199720172019Wrote 25 papers:
- PLDI-2015-CraryS #peer-to-peer #using
- Peer-to-peer affine commitment using bitcoin (KC, MJS), pp. 479–488.
- POPL-2015-CraryS #calculus #memory management
- A Calculus for Relaxed Memory (KC, MJS), pp. 623–636.
- ICFP-2010-Crary #higher-order #logic #representation
- Higher-order representation of substructural logics (KC), pp. 131–142.
- POPL-2007-LeeCH #ml #standard #towards
- Towards a mechanized metatheory of standard ML (DKL, KC, RH), pp. 173–184.
- CSL-2005-VIICH #control flow #distributed #logic
- Distributed Control Flow with Classical Modal Logic (TMV, KC, RH), pp. 51–69.
- ICLP-2005-SarkarPC #proving
- Small Proof Witnesses for LF (SS, BP, KC), pp. 387–401.
- LICS-2004-VIICHP #distributed #symmetry #λ-calculus
- A Symmetric Modal λ Calculus for Distributed Computing (TMV, KC, RH, FP), pp. 286–295.
- CADE-2003-CraryS #framework #logic
- Foundational Certified Code in a Metalogical Framework (KC, SS), pp. 106–120.
- POPL-2003-Crary #assembly #towards
- Toward a foundational typed assembly language (KC), pp. 198–212.
- POPL-2003-DreyerCH #higher-order #type system
- A type system for higher-order modules (DD, KC, RH), pp. 236–249.
- POPL-2003-PetersenHCP #layout #memory management #type system
- A type theory for memory allocation and data layout (LP, RH, KC, FP), pp. 172–184.
- ICFP-2002-CraryV #scalability #type system
- An expressive, scalable type theory for certified code (KC, JV), pp. 191–205.
- ICFP-2000-Crary #compilation #type system
- Typed compilation of inclusive subtyping (KC), pp. 68–81.
- POPL-2000-CraryW #bound #certification
- Resource Bound Certification (KC, SW), pp. 184–198.
- ICALP-1999-CraryM #low level #programming language
- Type Structure for Low-Level Programming Languages (KC, JGM), pp. 40–54.
- ICFP-1999-Crary #parametricity #proving
- A Simple Proof Technique for Certain Parametricity Results (KC), pp. 82–89.
- ICFP-1999-CraryW #analysis #flexibility
- Flexible Type Analysis (KC, SW), pp. 233–248.
- PLDI-1999-CraryHP #question #recursion #what
- What is a Recursive Module? (KC, RH, SP), pp. 50–63.
- POPL-1999-CraryWM #calculus #memory management
- Typed Memory Management in a Calculus of Capabilities (KC, DW, JGM), pp. 262–275.
- CADE-1998-Crary #fixpoint #induction
- Admissibility of Fixpoint Induction over Partial Types (KC), pp. 270–285.
- ICFP-1998-CraryWM #morphism #polymorphism #semantics
- Intensional Polymorphism in Type-Erasure Semantics (KC, SW, JGM), pp. 301–312.
- POPL-1998-MorrisettWCG #assembly #system f
- From System F to Typed Assembly Language (JGM, DW, KC, NG), pp. 85–97.
- ICFP-1997-Crary #higher-order #implementation #type system
- Foundations for the Implementation of Higher-Order Subtyping (KC), pp. 125–135.
- POPL-2017-Crary #abstraction #morphism #parametricity #polymorphism
- Modules, abstraction, and parametric polymorphism (KC), pp. 100–113.
- POPL-2019-Crary #compilation
- Fully abstract module compilation (KC), p. 29.