Research Papers

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

Types and Programming Languages

• Harrison Grodin, Runming Li, and Robert Harper. Abstraction Functions as Types. February, 2025.
• Yue Niu, Jonathan Sterling, and Robert Harper. Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory.
  MFPS 2024 Paper. MFPS 2024 Talk.
• Yue Niu and Robert Harper. A metalanguage for cost-aware denotational semantics. LICS 2023.
• Harrison Grodin and Robert Harper. Amortized Analysis via Coinduction.
  Preprint, March 2023.
• Jonathan Sterling and Robert Harper. Termination-Insensitive Non-Interference.
  FSCD 2022, August 2022.
• Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. Calf: A Cost-Aware Logical Framework. ACM SIGPLAN Symposium on Principles of Programming Languages, January 2022. PDF
• Jonathan Sterling and Robert Harper. Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
  J.ACM v.68, n.6, pp 1-47, 2021.
• Jonathan Sterling and Robert Harper. Guarded Computational Type Theory.
  Abstract. Short PDF. Long PDF.
• Daniel R. Licata and Robert Harper. A Monadic Formalization of ML5 (Preliminary Version).
  Abstract. PDF.
• Daniel R. Licata and Robert Harper. An Extensible Theory of Indexed Types.
  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.
• 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.
• Robert Harper and John C. Mitchell and Eugenio Moggi.
  Higher-Order Modules and the Phase Distinction.
  ACM POPL 1992.
  POPL PDF. TR PDF.

Higher Type Theory

• Evan Cavallo and Robert Harper.
  Internal Parametricity for Cubical Type Theory.
  arXiv preprint.
  CSL20.
  Revised and expanded version.
  
• Carlo Angiuli and Evan Cavallo and Kuen-Bang Hou (Favonia) and Robert Harper and John Sterling.
  The RedPRL Proof Assistant.
  Abstract.
  LFMTP18 Paper.
  
• Evan Cavallo and Robert Harper.
  Cubical Computationa Semantics for Higher Inductive Types.
  Errata in PoPL proceedings.
  Abstract.
  Paper.
  
• Carlo Angiuli and Kuen-Bang Hou (Favonia) and Robert Harper.
  Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.
  Abstract.
  Paper.
  
• Evan Cavallo and Robert Harper.
  Computational Higher Type Theory IV: Inductive Types.
  arXiv.
• Kuen-Bang Hou (Favonia) and Robert Harper.
  Covering Spaces in Homotopy Type Theory.
  Abstract.
  PDF.
  
• Carlo Angiuli and Kuen-Bang Hou (Favonia) and Robert Harper
  Computational Higher Type Theory III: Univalence and Universes.
  arXiv.
• Carlo Angiuli and Guillaume Brunerie and Thierry Coquand and Robert Harper and Kuen-Bang Hou (Favonia) and Daniel R. Licata
  Syntax and Models of Cartesian Cubical Type Theory.
  MSCS.
  
• Carlo Angiuli and Robert Harper.
  Meaning explanations at higher dimension.
  Abstract.
  PDF.
• Carlo Angiuli and Robert Harper and Todd Wilson
  Computational Higher Dimensional Type Theory.
  Abstract.
  PDF.
• Carlo Angiuli and Robert Harper
  Computational Higher Type Theory II: Dependent Cubical Realizability.
  arXiv.
• Carlo Angiuli, Robert Harper, and Todd Wilson
  Computational Higher Type Theory I: Abstract Cubical Realizability.
  arXiv.
• Steve Awodey and Robert Harper
  Homotopy Type Theory: Unified Foundations of Mathematics and Computation.
  Solicited survey article for the SIGLOG Newsletter, January 2015.
  PDF.
• Robert Harper and Kuen-Bang Hou (Favonia). A Note on the Uniform Kan Condition in Nominal Cubical Sets.
  PDF, arXiv.
• Carlo Angiuli, Ed Morehouse, Daniel R. Licata, and Robert Harper. Homotopical Patch Theory.
  ICFP 2014, Gothenburg, October, 2014.
  Abstract. ICFP PDF. Expanded Version with Appendix. Revised and expanded version.
• Daniel R. Licata and Robert Harper. Canonicity for 2-Dimensional Type Theory.
  Abstract. PDF.
• Robert Harper. Foundations and Applications of Higher-Dimensional Directed Type Theory.
  Project Description.
• Daniel R. Licata and Robert Harper. 2-Dimensional Directed Type Theory.
  Preliminary Draft PDF. Revised Draft PDF.

Types and Compilation

• Adam Chlipala, Leaf Petersen, and Robert Harper. Strict Bidirectional Type Checking. Types in Language Design andImplementation.
  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.
• Daniel Spoonhower, Guy E. Blelloch, and Robert Harper.
  Using Page Residencey to Balance Tradeoffs in Tracing Garbage Collection.
  Virtual Execution Environments'05
  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.

Type Refinements

• Robert Harper. Exception Tracking in an Open World.
  Theoretical Computer Science, September 2018.
• Kuen-Bang Hou (Favonia), Nick Benton, and Robert Harper. Correctness of Compiling Polymorphism to Dynamic Typing.
  Journal of Functional Programming, vol 27, December, 2016.
  JFP.
• Robert Harper and Rowan Davies. Refining Objects (Preliminary Summary).
  To appear, Luca Cardelli 60th Birthday Celebration, Cambridge, October, 2014.
  Abstract. LC60 PDF.
• Yitzhak Mandelbaum, David Walker, and Robert Harper. An Effective Theory of Type Refinements.
  ICFP '03.
  Citation. Abstract. TR PDF. ICFP PDF.

Mechanized Metatheory

• Karl Crary and Robert Harper, Mechanized Definition of Standard ML
  
• 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. Twelf
• Robert Harper and Daniel Licata
  Mechanizing Metatheory in a Logical Framework.
  To appear, Journal of Functional Programming, 2007.
  Citation. PDF. Twelf Code.

Logical Frameworks

• Robert Harper. An Equational Logical Framework for Type Theories, June 2021.
  arXiv.
• Robert Harper. Notes on Logical Frameworks, January 2021.
  PDF.
• Karl Crary and Robert Harper
  Higher-Order Abstract Syntax: Setting the Record Straight.
  SIGACT News Logic Column 16, July 2006.
• Daniel R. Licata and Robert Harper
  A Universe of Binding and Computation.
  Short PDF. Abstract. BibTeX. Agda Code.
• Daniel R. Licata and Robert Harper
  Positively Dependent Types.
  Short PDF. Abstract. Citation.
• Daniel R. Licata and Robert Harper
  Dependently Typed Programming With Domain-Specific Logics.
  Short PDF. Abstract. BibTeX.
• Daniel R. Licata, Noam Zeilberger, and Robert Harper
  Focusing on Binding and Computation.
  Citation. Full PDF. Short PDF.
• 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 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.
• 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.28 n.6, 2006.
  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

Verification of Concurrent and Probabilistic Programs

• Joseph Tassarotti and Robert Harper.
  A Separation Logic for Concurrent Randomized Programs.
  Abstract. PDF.
• Joseph Tassarotti and Robert Harper.
  Verified Tail Bounds for Randomized Programs.
  Abstract. ITP 2018.
• Joseph Tassarotti and Ralf Jung and Robert Harper.
  A Higher-Order Logic for Concurrent Termination-Preserving Refinement.
  Preprint
  

Parallelism and Cost Semantics

• Stefan K. Muller, Umut A. Acard, and Robert Harper.
  Competitive Parallelism: Getting Your Priorities Right.
  Abstract PDF Publication Version arXiv Full Version
• Ananya Kumar and Guy E. Blelloch and Robert Harper.
  Parallel Functional Arrays.
  Abstract
  POPL 2017
• Stefan K. Muller and Umut A. Acar and Robert Harper.
  Responsive Parallel Computation: Bridging Competitive and Cooperative Threading.
  Abstract
  PLDI 2017
• Robert Harper.
  Structure and Efficiency of Computer Programs.
  PDF.
  Position paper submitted to NSF, July, 2014.
• Guy E. Blelloch and Robert Harper. Cache and I/O Efficient Functional Algorithms.
  Abstract. POPL PDF.
• Guy E. Blelloch and Robert Harper. Cache Efficient Functional Algorithms.
  Abstract. CACM PDF.
• Daniel Spoonhower and Guy E. Blelloch and Robert Harper and Phillip B. Gibbons, Beyond Nested Parallelism: Tight Bounds on Work-Stealing Overheads for Parallel Futures.
  Citation. PDF. Abstract.
• Daniel Spoonhower and Guy E. Blelloch and Phillip B. Gibbons and Robert Harper. Space Profiling for Parallel Functional Programs.
  Short PDF. Long PDF. Abstract. JFP Article.
• Daniel Spoonhower, Guy E. Blelloch, and Robert Harper. A Semantic Framework for Scheduling Parallel Programs.
  Citation. Paper.

Security

• Kumar Avijit and Anupam Datta and Robert Harper, Distributed Programming with Distributed Authorization.
  Types in Language Design and Implementation (TLDI), Madrid, Spain, January 2010.
  Abstract. Short PDF.
• Avijit Kumar and Robert Harper. A Language for Access Control.
  Citation. Abstract. Paper.
• 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.
• Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, and Stephan Zdancewic.
  Manifest Security.
  January, 2007.
  PDF.

Other Topics

• David MacQueen, Robert Harper, and John Reppy.
  The History of Standard ML
  PDF on SML Family web site.
• Robert Harper.
  Cambridge University Press Author's Blog Essay, April, 2017.
  What, if anything, is a programming paradigm?.
• Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion Kolaitis, Moshe Y. Vardi, and Victor Vianu.
  On the Unusual 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.
• 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
• Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, and Peter Sewell.
  Robin Milner 1934--2010: Verification, Languages, and Concurrency.
  January, 2011.
  PDF
• Guy E. Blelloch and Robert Harper.
  λ-Calculus: The Other Turing Machine.
  To appear, CMU CSD 50th Anniversary volume, September, 2015.
  PDF
• Jonathan Sterling and Robert Harper.
  Algebraic Foundations of Proof Refinement.
  March, 2017.
  arXiv.

Last modified: Thu Sep 30 19:16:32 EDT 2021