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 Papers
Research Papers
These are most of my research papers, grouped by rough subject
classifications.
Types and Language Design
Daniel Spoonhower and Guy E. Blelloch and Phillip B. Gibbons and Robert Harper.
Space Profiling for Parallel Functional Programs. Short PDF.
Abstract.
Daniel R. Licata and Robert Harper.
An Extensible Theory of Indexed Types. Citation.
Abstract.
Paper.
Daniel Spoonhower, Guy E. Blelloch, and Robert Harper.
A Semantic Framework for Scheduling Parallel Programs. Citation.
Paper.
Avijit Kumar and Robert Harper.
A Language for Access Control. Citation.
Abstract.
Paper.
Karl Crary and Robert Harper.
Syntactic Logical Relations for Polymorphic and Recursive
Types. Citation.
PDF.
Derek Dreyer, Robert Harper,
and Manuel Chakravarty. Modular Type Classes. Citation.
Short PDF.
Full PDF.
David Swasey, Tom
Murphy VII, Karl Crary, and Robert Harper. A Separate
Compilation Extension to Standard ML. PDF.
TR Citation.
TR PDF.
Daniel R. Licata and Robert
Harper. A Formulation of Dependent ML with Explicit
Equality Proofs. Citation.
PDF.
Derek Dreyer, Robert
Harper, and Karl Crary. A Type System for Safe
Recursion.
Technical Report CMU-CS-03-163, August, 2003. Citation.
TR PS. TR PDF.
Yitzhak Mandelbaum, David
Walker, and Robert Harper. An Effective Theory of Type
Refinements.
ICFP '03. Citation. Abstract. TR PDF. ICFP PDF.
Joseph C.
Vanderwaart, Derek R. Dreyer, Leaf Petersen, Karl Crary, Robert
Harper, and Perry Cheng. Typed Compilation of Recursive
Datatypes.
TLDI '03: 2003 ACM SIGPLAN International Workshop on Types in
Language Design and Implementation. Citation. Abstract. Short PS. Short PDF. Long PDF.
Derek Dreyer, Karl Crary,
and Robert Harper. A Type Theory for Higher-Order
Modules.
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, New Orleans, LA, January, 2003. Citation. Abstract. Short PDF. Long PDF.
Derek Dreyer, Robert
Harper, and Karl Crary.
Towards a Practical Type Theory for Recursive
Modules.
Technical Report. March, 2001. Citation. Abstract. PS. PDF.
The ML2000 Working
Group.
Principles and a Preliminary Design for
ML2000.
Draft. July, 1999. Citation. Abstract. PS. PDF.
John C. Mitchell and Robert Harper.
Parametricity and Variants of Girard's J
Operator.
Information Processing Letters. 1999. Citation. Abstract. PS. PDF.
Karl Crary, Robert Harper, Perry Cheng, Leaf Petersen, and
Chris Stone.
Transparent and Opaque Interpretations of Data
Types.
Technical Report. November, 1998. Citation. Abstract. PS. PDF.
Karl Crary, Robert Harper,
and Sidd Puri.
What is a Recursive Module?
PLDI. October, 1998. Citation. Abstract. PS. PDF.
Lars Birkedal and Robert Harper.
Relational Interpretations of Recursive Types in an
Operational Setting.
Information and Computation. 1998. Citation. Abstract. PS. PDF.
Mark Lillibridge and Robert Harper.
A Type-Theoretic Approach to Higher-Order Modules with
Sharing.
POPL. January, 1994. Citation. Abstract. PS. PDF.
Robert Harper.
A Simplified Account of Polymorphic
References.
Information Processing Letters. 1994. Citation. Abstract. PS. PDF.
Robert Harper, Bruce Duba, and David B. MacQueen.
Typing First-Class Continuations in ML.
Journal of Functional Programming. October, 1993. Citation. Abstract. PS. PDF.
Robert Harper and John C. Mitchell.
On the Type Structure of Standard ML.
TOPLAS. 1993. Citation. Abstract. PS. PDF.
Types and Compilation
Adam Chlipala, Leaf
Petersen, and Robert Harper. Strict Bidirectional Type
Checking. Types in Language Design and
Implementation. Citation. Abstract. PDF.
David Tarditi, Greg
Morrisett, Perry Cheng, Chris Stone, Robert Harper, and Peter
Lee. Retrospective on TIL: A Type-Directed, Optimizing
Compiler for ML. 20 Years of the ACM/SIGPLAN
Conference on Programming Language Design and Implementation
(1979-1999): A Selection. Citation. Abstract. PDF.
Leaf Petersen, Robert
Harper, Karl Crary, Frank Pfenning. A Type Theory for
Memory Allocation and Data Layout.
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, New Orleans, LA, January, 2003. Citation. Abstract. PDF.
Leaf Petersen, Perry
Cheng, Robert Harper, and Chris Stone.
Implementing the TILT Internal Language.
Technical Report. 2001.
Chris Stone and Robert Harper.
A Type-Theoretic Interpretation of Standard
ML.
Milner Festschrifft. 2000. Citation. PS. PDF.
Chris Stone and
Robert Harper.
Decidable Type Equivalence in a Language with Singleton
Kinds.
POPL. January, 1999. Citation. Abstract. PS. PDF.
Technical Report. August, 1999. Citation.
Abstract.
PS. PDF.
ACM Transactions on Computational Logic, v.7, n.4, October, 2006.
Extensional Equivalence and Singleton Types. Citation. PDF.
Andrew Bernard, Robert Harper, and Peter Lee.
How Generic is a Generic Back End? Using MLRISC as a Back
End for the TIL Compiler.
TIC 1998. Citation. Abstract. PS. PDF.
Greg Morrisett and Robert Harper.
Semantics of Memory Management for Polymorphic
Languages.
HOOTS 1998. Citation. Abstract. PS. PDF.
Greg Morrisett and Robert Harper.
Typed Closure Conversion for Recursively Defined
Functions (Extended Abstract).
HOOTS. 1997. Citation. Abstract. PS. PDF.
Robert Harper and Chris Stone.
An Interpretation of Standard ML in Type
Theory.
Technical Report. June, 1997. Citation. Abstract. PS. PDF.
David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone,
Robert Harper, and Peter Lee.
TIL: A Type-Directed Optimizing Compiler for
ML.
PLDI. 1996. Citation. PS. PDF.
Technical Report. February, 1996. Citation. PS. PDF.
Greg Morrisett, David Tarditi, Perry Cheng, Chris Stone,
Robert Harper, and Peter Lee.
TIL: Performance and Safety Through Types.
Workshop on Compiler Support for Systems Software. 1996. Citation. PS. PDF.
Yasuhiko Minamide, Greg Morrisett, and Robert Harper.
Typed Closure Conversion.
POPL 1996. Citation. Abstract. PS. PDF.
Robert Harper and Mark Lillibridge.
Operational Interpretation of an Extension of $F_\omega$
with Control Operators.
Journal of Functional Programming. 1996. Citation.
Abstract.
PS. PDF.
Greg Morrisett, Matthias Felleisen, and Robert
Harper.
Abstract Models of Memory Management.
FPCA 1995. Citation. Abstract. PS. PDF.
Robert Harper and Greg Morrisett.
Compiling Polymorphism Using Intensional Type
Analysis.
POPL 1995. Citation.
Abstract.
PS. PDF.
Robert Harper and Mark Lillibridge.
Explicit Polymorphism and CPS Conversion.
POPL 1993. Citation.
Abstract.
PS. PDF.
Robert Harper and Mark Lillibridge.
Polymorphic Type Assignment and CPS
Conversion.
LISP and Symbolic Computation. 1993. Citation. Abstract. PS. PDF. Correction (PDF).
Certifying Compilers
Hongwei Xi and Robert
Harper.
A Dependently Typed Assembly Language.
Proc. ICFP, Florence, Italy. September, 2001. Citation. Abstract. PS. PDF.
Christopher Colby,
Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
Automated Techniques for Provably Safe Mobile
Code.
Theoretical Computer Science (Special Issue on Dependable
Computing), v.~290, n.~2, January, 2003, pp. 1175-1199 Citation. Abstract. PS. PDF.
Fred B. Schneider, Greg
Morrisett, and Robert Harper.
A Language-Based Approach to Security.
Informatics: Ten Years Back, Ten Years Ahead. Springer LNCS v.2000,
2000. Citation. Abstract. PS. PDF.
Logical Frameworks
Daniel R. Licata and Robert Harper
Dependently Typed Programming With Domain-Specific Logics. Short PDF.
Abstract.
Daniel R. Licata, Noam Zeilberger, and Robert Harper
Focusing on Binding and Computation. Citation.
Full PDF.
Short PDF.
Daniel K. Lee, Karl Crary, and Robert Harper
Towards a Mechanized Metatheory of Standard ML.
ACM POPL 2007, Nice, France. Citation.
Short PDF.
Full PDF.
Robert Harper and Daniel
Licata
Mechanizing Metatheory in a Logical Framework.
To appear, Journal of Functional Programming, 2007. Citation.
PDF.
Twelf Code.
Robert Harper and
Frank Pfenning.
On Equivalence and Canonical Forms in the LF Type
Theory.
To appear: ACM Trans. Comp. Logic, 2004. Citation. Abstract. PS. PDF.
Workshop on Logical Frameworks and Meta-languages. Paris,
1999. Citation.
PS. PDF.
Robert Harper, Furio Honsell, and Gordon Plotkin.
A Framework for Defining Logics.
Journal of the ACM. 1993. Citation. Abstract. PS. PDF.
Robert Harper and Karl
Crary
How To Believe a Twelf Proof. PDF.
Scientific Computing
Aleksandar Nanevski,
Guy Blelloch, and Robert Harper.
Automatic Generation of Staged Geometric
Predicates.
Technical Report. June, 2001. Citation. Abstract. PS. PDF.
Proc. ICFP, Florence, Italy, September, 2001. Citation. Abstract. PS. PDF.
Journal of Higher-Order and Symbolic
Computation. Final
Version.
Guy
Blelloch, Hal Burch, Karl Crary, Robert Harper, Gary Miller,
and Noel Walkington.
Persistent Triangulations.
Journal of Functional Programming, volume 11, part 5.
September, 2001. Citation. Abstract. PS. PDF.
S. A. Seshia, G. E. Blelloch, and R. W. Harper.
A Performance Comparison of Interval Arithmetic and Error
Analysis for Geometric Predicates.
Technical Report. 2001. Citation. Abstract. PS. PDF.
Computation and Information Grids
Type-Safe Distributed Programming with ML5.
Tom Murphy VII, Karl Crary, and Robert Harper.
November, 2007. Citation.
PDF.
Multiscale Scheduling, Integrating Competitive and
Cooperative Parallelism in Theory and in Practice.
G. E. Blelloch, L. Blum, M. Harchol-Balter, and R. Harper.
February, 2007. PDF.
Manifest Security.
Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce,
Stephanie Weirich, and Stephan Zdancewic.
January, 2007. PDF.
Distributed Control Flow
with Classical Modal Logic.
Tom Murphy VII, Karl Crary, and Robert Harper.
CSL '05, Oxford, England Citation. Abstract. PDF.
A Symmetric Modal Lambda
Calculus for Distributed Computing.
Tom Murphy VII, Karl Crary, Robert Harper, Frank
Pfenning.
Nineteenth IEEE Symposium on Logic in Computer Science, Turku,
Finland, July, 2004. Citation. Abstract. PS. PDF.
Carnegie Mellon University Technical Report CMU-CS-04-105,
February, 2004. Citation. Abstract. PS. PDF.
Trustless Grid Computing in
ConCert.
Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper,
Jason Liszka, Tom Murphy VII, Frank Pfenning.
GRID 2002, Baltimore, MD, November, 2002. Citation. PS. PDF.
Umut A. Acar, Guy E. Blelloch,
and Robert Harper.
Adaptive Functional Programming.
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, Portland, January 2002. Citation. Abstract. PS. PDF.
ACM Transactions on Programming Languages and Systems, v.? n.?,
2006. (To appear.) Citation. Abstract. PDF.
Carnegie Mellon University Computer Science Department
Technical Report CMU-CS-01-161, December, 2001. PS. PDF.
Umut Acar, Guy
Blelloch, and Robert Harper. Selective
Memoization.
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, New Orleans, LA, January, 2003. Citation.
Abstract.
PDF.
Umut A.
Acar, Guy E. Blelloch, Robert Harper, Jorge L. Vittes, and Shan
Leung Maverick Woo.
Dynamizing Static Algorithms, with Applications to
Dynamic Trees and History Independence.
ACM-SIAM Sympsosium on Discrete Algorithms, New Orleans,
January, 2004. Citation.
Abstract.
PS. PDF.
Umut A. Acar, Guy E. Blelloch,
Matthias Blume, and Robert Harper.
Self-Adjusting Programming.
ML Workshop 2005, Tallinn, Estonia, September, 2005. CitationPDF
Other Topics
Joseph Y. Halpern,
Robert Harper, Neil Immerman, Phokion Kolaitis, Moshe Y. Vardi,
and Victor Vianu.
On the Unsual Effectiveness of Logic in Computer
Science.
Bulletin of Symbolic Logic. 2001. Citation. PS. PDF.
Edoardo Biagioni, Robert
Harper, and Peter Lee.
A Network Protocol Stack in Standard ML.
Higher Order and Symbolic Computation. 2001. Citation. Abstract. PDF.
Robert Harper.
Proof-Directed Debugging.
Journal of Functional Programming. 2000. Citation. Abstract. PS. PDF.
Daniel Spoonhower, Guy E.
Blelloch, and Robert Harper.
Using Page Residencey to Balance Tradeoffs in Tracing
Garbage Collection.
April, 2005. To appear, Virtual Execution Environments
'05 PDF
Tom Murphy VII, Daniel Spoonhower,
Chris Casinghino, Daniel R. Licata, Karl Crary and Robert Harper.
The Cult of the Bound Variable: The 9th Annual ICFP Programming
Contest.
September, 2006. PDF