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.
  ML Workshop Citation. ML WorkshopPDF. Technical Report Citation. Technical Report.
• 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.
  
  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 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.
  
  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.
  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.
• 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 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, 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.
  ML Workshop 2005, Tallinn, Estonia, September, 2005.
  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
• 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

Last modified: Wed Jul 2 13:57:13 EDT 2008