Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Karl Crary's papers
Papers
Latest Publications
Karl Crary.
Explicit Contexts in LF.
2008 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.
(pdf, twelf)
Karl Crary and Robert Harper.
Syntactic Logical Relations for Polymorphic and Recursive Types.Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, 2007.
(pdf)
Daniel K. Lee, Karl Crary, and Robert Harper.
Mechanizing the Metatheory of Standard ML.2006 Symposium on Principles of Programming Languages.
(pdf, twelf)
Karl Crary and Susmit Sarkar.
Foundational Certified Code in a Metalogical Framework.ACM Transactions on Computational Logic, to appear.
(pdf)
Karl Crary.
Sound and Complete Elimination of Singleton Kinds.ACM Transactions on Computational Logic, 2007.
(pdf)
Susmit Sarkar, Brigitte Pientka, and Karl Crary.
Small Proof Witnesses for LF.2005 International Conference on Logic Programming.
(pdf)
Tom Murphy VII, Karl Crary, and Robert Harper.
Distributed Control Flow with Classical Modal Logic.2005 Computer Science Logic.
(pdf)
Karl Crary, Aleksey Kliger, and Frank Pfenning.
A Monadic Analysis of Information Flow Security with Mutable State.Journal of Functional Programming: Special issue on Language-Based Security, March 2005.
(pdf)
Karl Crary.
Logical Relations and a Case Study in Equivalence Checking.Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, 2005.
Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning.
A Symmetric Modal Lambda Calculus for Distributed Computing.2004 Symposium on Logic in Computer Science.
(pdf)
Expanded Version.CMU Technical Report CMU-CS-04-105.
(pdf)
Karl Crary.
Toward a Foundational Typed Assembly Language.2003 Symposium on Principles of Programming Languages.
(ps,
pdf)
Expanded Version.CMU Technical Report CMU-CS-02-196.
(ps,
pdf)
Derek Dreyer, Karl Crary, and Robert Harper.
A Type System for Higher-Order Modules.2003 Symposium on Principles of Programming Languages.
(ps,
pdf)
Expanded Version.CMU Technical Report CMU-CS-02-122R.
(ps,
pdf)
Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning.
A Type Theory for Memory Allocation and Data Layout.2003 Symposium on Principles of Programming Languages.
(ps,
pdf)
Expanded Version.CMU Technical Report CMU-CS-02-171.
(ps,
pdf)
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert
Harper, and Perry Cheng.
Typed Compilation of Recursive Datatypes.2003 Workshop on Types in Language Design and Implementation.
(ps,
pdf)
Joseph C. Vanderwaart and Karl Crary.
A Typed Interface for Garbage Collection.2003 Workshop on Types in Language Design and Implementation.
(ps,
pdf)
Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason
Liszka, Tom Murphy VII, and Frank Pfenning.
Trustless Grid Computing in ConCert.2002 International Workshop on Grid Computing.
(ps,
pdf)
Karl Crary and Joseph C. Vanderwaart.
An Expressive, Scalable Type Theory for Certified Code.2002 International Conference on Functional Programming.
(ps,
pdf)
Joseph C. Vanderwaart and Karl Crary.
A Simplified Account of the Metatheory of Linear LF.CMU Technical Report CMU-CS-01-154.
(ps,
pdf)
Short Version.2002 International Workshop on Logical Frameworks and Meta-Languages.
(ps)
Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type-Erasure Semantics.Journal of Functional Programming, November 2002.
(ps)
Greg Morrisett, Karl Crary, Neal Glew, and David Walker.
Stack-Based Typed Assembly Language.Journal of Functional Programming, January 2002.
(abstract,
ps)
Guy Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller, and Noel Walkington.
Persistent Triangulations.Journal of Functional Programming, September 2001.
(pdf)
David Walker, Karl Crary, and Greg Morrisett.
Typed Memory Management via Static Capabilities.ACM TOPLAS, July 2000.
(abstract,
ps,
pdf)
Michael Hicks, Stephanie Weirich, and Karl Crary.
Safe and Flexible Dynamic Linking of Native Code.2000 Workshop on Types in Compilation.
(abstract,
pdf)
Karl Crary.
Typed Compilation of Inclusive Subtyping.2000 International Conference on Functional Programming.
(abstract,
ps)
Karl Crary and Stephanie Weirich.
Resource Bound Certification.2000 Symposium on Principles of Programming Languages.
(abstract,
ps.gz,
dvi)
Karl Crary and Stephanie Weirich.
Flexible Type Analysis.1999 International Conference on Functional Programming.
(abstract,
ps.gz,
dvi)
Karl Crary.
A Simple Proof Technique for Certain Parametricity Results.1999 International Conference on Functional Programming.
(abstract,
ps.gz,
dvi)
Karl Crary and Greg Morrisett.
Type Structure for Low-Level Programming Languages.1999 International Colloquium on Automata, Languages, and Programming.
(abstract,
ps.gz,
dvi)
Karl Crary, Robert Harper, and Sidd Puri.
What is a Recursive Module?1999 Conference on Programming Language Design and Implementation.
(abstract,
ps.gz,
dvi)
Greg Morrisett, David Walker, Karl Crary, and Neal Glew.
From System F to Typed Assembly Language.ACM TOPLAS, May 1999.
(abstract,
ps)