Karl Crary - RankMe

62 papers A* 14A 9B 3C 1Journal 18Unranked 15

Year	Rank	Type	Title / Venue / Authors
2025	B	`conf`	Substructural Parametricity. FSCD C. B. Aberlé, Karl Crary, Chris Martens, Frank Pfenning
2021	J	`jnl`	Verifying the Hashgraph Consensus Algorithm. CoRR Karl Crary
2020	J	`jnl`	A focused solution to the avoidance problem. J. Funct. Program. Karl Crary
2019	J	`jnl`	Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrency. CoRR Michael J. Sullivan, Karl Crary, Salil Joshi
2019	J	`jnl`	Fully abstract module compilation. Proc. ACM Program. Lang. Karl Crary
2018	C	`conf`	Hygienic Source-Code Generation Using Functors - (Extended Abstract). PADL Karl Crary
2018	J	`jnl`	Hygienic Source-Code Generation Using Functors. CoRR Karl Crary
2018	A*	`conf`	Strong Sums in Focused Logic. LICS Karl Crary
2018	—	`conf`	TWAM: A Certifying Abstract Machine for Logic Programs. VSTTE Rose Bohrer, Karl Crary
2018	J	`jnl`	TWAM: A Certifying Abstract Machine for Logic Programs. CoRR Rose Bohrer, Karl Crary
2017	A*	`conf`	Modules, abstraction, and parametric polymorphism. POPL Karl Crary
2015	A*	`conf`	A Calculus for Relaxed Memory. POPL Karl Crary, Michael J. Sullivan
2015	A*	`conf`	Peer-to-peer affine commitment using bitcoin. PLDI Karl Crary, Michael J. Sullivan
2010	A	`conf`	Higher-order representation of substructural logics. ICFP Karl Crary
2010	—	`ed.`	Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010. LFMTP Karl Crary, Marino Miculan
2009	—	`conf`	A syntactic account of singleton types via hereditary substitution. LFMTP Karl Crary
2008	—	`conf`	Explicit Contexts in LF (Extended Abstract). LFMTP@LICS Karl Crary
2008	J	`jnl`	Foundational certified code in the Twelf metalogical framework. ACM Trans. Comput. Log. Karl Crary, Susmit Sarkar
2007	J	`jnl`	Sound and complete elimination of singleton kinds. ACM Trans. Comput. Log. Karl Crary
2007	—	`conf`	Syntactic Logical Relations for Polymorphic and Recursive Types. Computation, Meaning, and Logic Karl Crary, Robert Harper
2007	A*	`conf`	Towards a mechanized metatheory of standard ML. POPL Daniel K. Lee, Karl Crary, Robert Harper
2007	—	`conf`	Type-Safe Distributed Programming with ML5. TGC Tom Murphy VII, Karl Crary, Robert Harper
2006	—	`conf`	A separate compilation extension to standard ML. ML David Swasey, Tom Murphy VII, Karl Crary, Robert Harper
2006	J	`jnl`	Higher-order abstract syntax: setting the record straight. SIGACT News Karl Crary, Robert Harper
2006	J	`jnl`	Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight CoRR Karl Crary, Robert Harper
2005	J	`jnl`	A monadic analysis of information flow security with mutable state. J. Funct. Program. Karl Crary, Aleksey Kliger, Frank Pfenning
2005	—	`conf`	Automated and certified conformance to responsiveness policies. TLDI Joseph Vanderwaart, Karl Crary
2005	B	`conf`	Distributed Control Flow with Classical Modal Logic. CSL Tom Murphy VII, Karl Crary, Robert Harper
2005	B	`conf`	Small Proof Witnesses for LF. ICLP Susmit Sarkar, Brigitte Pientka, Karl Crary
2004	A*	`conf`	A Symmetric Modal Lambda Calculus for Distributed Computing. LICS Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
2003	A*	`conf`	A type system for higher-order modules. POPL Derek Dreyer, Karl Crary, Robert Harper
2003	A*	`conf`	A type theory for memory allocation and data layout. POPL Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
2003	—	`conf`	A typed interface for garbage collection. TLDI Joseph Vanderwaart, Karl Crary
2003	J	`jnl`	Automated techniques for provably safe mobile code. Theor. Comput. Sci. Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
2003	A	`conf`	Foundational Certified Code in a Metalogical Framework. CADE Karl Crary, Susmit Sarkar
2003	J	`jnl`	Stack-based typed assembly language. J. Funct. Program. J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker
2003	A*	`conf`	Toward a foundational typed assembly language. POPL Karl Crary
2003	—	`conf`	Typed compilation of recursive datatypes. TLDI Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, Perry Cheng
2002	—	`conf`	A Simplified Account of the Metatheory of Linear LF. LFM Joseph Vanderwaart, Karl Crary
2002	A	`conf`	An expressive, scalable type theory for certified code. ICFP Karl Crary, Joseph Vanderwaart
2002	J	`jnl`	Intensional polymorphism in type-erasure semantics. J. Funct. Program. Karl Crary, Stephanie Weirich, J. Gregory Morrisett
2002	J	`jnl`	Stack-based typed assembly language. J. Funct. Program. J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker
2002	—	`conf`	Trustless Grid Computing in ConCert. GRID Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning
2001	J	`jnl`	Persistent triangulations Journal of Functional Programming. J. Funct. Program. Guy E. Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary L. Miller, Noel Walkington
2000	A*	`conf`	Resource Bound Certification. POPL Karl Crary, Stephanie Weirich
2000	—	`conf`	Safe and Flexible Dynamic Linking of Native Code. Types in Compilation Michael W. Hicks, Stephanie Weirich, Karl Crary
2000	—	`conf`	Sound and Complete Elimination of Singleton Kinds. Types in Compilation Karl Crary
2000	A	`conf`	Typed compilation of inclusive subtyping. ICFP Karl Crary
2000	J	`jnl`	Typed memory management via static capabilities. ACM Trans. Program. Lang. Syst. David Walker, Karl Crary, J. Gregory Morrisett
1999	A	`conf`	A Simple Proof Technique for Certain Parametricity Results. ICFP Karl Crary
1999	A	`conf`	Flexible Type Analysis. ICFP Karl Crary, Stephanie Weirich
1999	J	`jnl`	From system F to typed assembly language. ACM Trans. Program. Lang. Syst. J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew
1999	A*	`conf`	Type Structure for Low-Level Programming Languages. ICALP Karl Crary, J. Gregory Morrisett
1999	A*	`conf`	Typed Memory Management in a Calculus of Capabilities. POPL Karl Crary, David Walker, J. Gregory Morrisett
1999	A*	`conf`	What is a Recursive Module? PLDI Karl Crary, Robert Harper, Sidd Puri
1998	A	`conf`	Admissibility of Fixpoint Induction over Partial Types. CADE Karl Crary
1998	A*	`conf`	From System F to Typed Assembly Language. POPL J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew
1998	A	`conf`	Intensional Polymorphism in Type-Erasure Semantics. ICFP Karl Crary, Stephanie Weirich, J. Gregory Morrisett
1998	—	`conf`	Programming language semantics in foundational type theory. PROCOMET Karl Crary
1998	—	`conf`	Stack-Based Typed Assembly Language. Types in Compilation J. Gregory Morrisett, Karl Crary, Neal Glew, David Walker
1998	—	`—`	Type-Theoretic Methodology for Practical Programming Languages. Karl Crary
1997	A	`conf`	Foundations for the Implementation of Higher-Order Subtyping. ICFP Karl Crary