Research Papers

These are most of my research papers, grouped by rough subject classifications.

Types and Language Design

• 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.
  
  Addendum: 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.
  
  Technical report (expanded version).
  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 TOCL.
  Extensional Equivalence and Singleton Types. November, 2004.
  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.
  
  Technical Report, July, 1999.
  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.
  Dagstuhl 10th Anniversary Volume. 2000.
  Citation. Abstract. PS. PDF.

Logical Frameworks

• 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.

Grid Computing

• 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.
• A Symmetric Modal Lambda Calculus for Distributed Computing.
  Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning.
  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.
• Towards a Functional Library for Fault-Tolerant Grid Computing.
  Bor-Yuh Evan Chang, Margaret DeLap, Jason Liszka, Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning.
  Unpublished manuscript, May, 2002.
  Citation. PS. PDF.

Self-Adjusting Computation

• Umut Acar, Guy Blelloch, and Robert Harper.
  Adaptive Functional Programming.
  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, January 2002.
  Citation. Abstract. PS. PDF.
• Umut Acar, Guy E. Blelloch, and Robert Harper.
  Adaptive Functional Programming.
  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, and Robert Harper.
  Adaptive Memoization.
  Citation. Abstract. PDF (Short). PDF (Long).
• Umut A. Acar, Guy E. Blelloch, Matthias Blume, and Robert Harper.
  Self-Adjusting Programming.
  Citation PDF

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

Last modified: Wed Dec 14 18:25:46 EST 2005