| 2026 | CPP | Mechanizing Synthetic Tait Computability in Istari. | Runming Li, Yue Yao, Robert Harper |
| 2026 | ESOP | Recursive Logical Relations for Intuitionistic Linear Logic Session Types. | Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao |
| 2023 | CALCO | Integrating Cost and Behavior in Type Theory (Invited Talk). | Robert Harper |
| 2023 | CALCO | Amortized Analysis via Coinduction (Early Ideas). | Harrison Grodin, Robert Harper |
| 2023 | LICS | A Metalanguage for Cost-Aware Denotational Semantics. | Yue Niu, Robert Harper |
| 2023 | NOMS | Efficient Periodicity Analysis for Real-Time Anomaly Detection. | Yusufu Shehu, Robert Harper |
| 2022 | CNSM | Accelerating Causal Inference Based RCA Using Prior Knowledge From Functional Connectivity Inference. | Giles Winchester, George Parisis, Robert Harper, Luc Berthouze |
| 2022 | FSCD | Sheaf Semantics of Termination-Insensitive Noninterference. | Jonathan Sterling, Robert Harper |
| 2022 | NOMS | Structural Network Metrics and Incident Generation. | Robert Harper, Philip Tee |
| 2021 | IM | Exploring the Adaptability of Word Embeddings to Log Message Classification. | Yusufu Shehu, Robert Harper |
| 2020 | CSL | Internal Parametricity for Cubical Type Theory. | Evan Cavallo, Robert Harper |
| 2020 | NOMS | Improved Fault Localization using Transfer Learning and Language Modeling. | Yusufu Shehu, Robert Harper |
| 2019 | IM | A Method for Temporal Event Correlation. | Robert Harper, Philip Tee |
| 2019 | IM | Functional Topology Inference from Network Events. | Antoine Messager, George Parisis, Istvan Z. Kiss, Robert Harper, Phil Tee, Luc Berthouze |
| 2018 | CSL | Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. | Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper |
| 2018 | ITP | Verified Tail Bounds for Randomized Programs. | Joseph Tassarotti, Robert Harper |
| 2018 | LICS | Guarded Computational Type Theory. | Jonathan Sterling, Robert Harper |
| 2018 | NOMS | Cookbook, a recipe for fault localization. | Robert Harper, Philip Tee |
| 2018 | NOMS | Network events in a large commercial network: What can we learn? | Antoine Messager, George Parisis, Robert Harper, Philip Tee, Istvan Z. Kiss, Luc Berthouze |
| 2017 | ESOP | A Higher-Order Logic for Concurrent Termination-Preserving Refinement. | Joseph Tassarotti, Ralf Jung, Robert Harper |
| 2017 | IM | The application of Neural Networks to predicting the root cause of service failures. | Robert Harper, Philip Tee |
| 2017 | PLDI | Responsive parallel computation: bridging competitive and cooperative threading. | Stefan K. Muller, Umut A. Acar, Robert Harper |
| 2017 | POPL | Computational higher-dimensional type theory. | Carlo Angiuli, Robert Harper, Todd Wilson |
| 2017 | POPL | Parallel functional arrays. | Ananya Kumar, Guy E. Blelloch, Robert Harper |
| 2014 | ICFP | Homotopical patch theory. | Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper |
| 2013 | POPL | Cache and I/O efficent functional algorithms. | Guy E. Blelloch, Robert Harper |
| 2012 | POPL | Canonicity for 2-dimensional type theory. | Daniel R. Licata, Robert Harper |
| 2011 | POPL | Robin Milner 1934--2010: verification, languages, and concurrency. | Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell |
| 2009 | ICFP | A universe of binding and computation. | Daniel R. Licata, Robert Harper |
| 2009 | SIGCSE | Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report. | Mark W. Bailey, Kim B. Bruce, Kathleen Fisher, Robert Harper, Stuart Reges |
| 2009 | SPAA | Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures. | Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, Robert Harper |
| 2008 | ICFP | Space profiling for parallel functional programs. | Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons |
| 2008 | LICS | Focusing on Binding and Computation. | Daniel R. Licata, Noam Zeilberger, Robert Harper |
| 2007 | POPL | Modular type classes. | Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller |
| 2007 | POPL | Towards a mechanized metatheory of standard ML. | Daniel K. Lee, Karl Crary, Robert Harper |
| 2006 | CBMS | PsyGrid: Applying e-Science to Epidemiology. | John D. Ainsworth, Robert Harper, Ismael Juma, Iain E. Buchan |
| 2005 | CSL | Distributed Control Flow with Classical Modal Logic. | Tom Murphy VII, Karl Crary, Robert Harper |
| 2005 | ICFP | Mechanizing the meta-theory of programming languages. | Robert Harper |
| 2005 | VEE | Using page residency to balance tradeoffs in tracing garbage collection. | Daniel Spoonhower, Guy E. Blelloch, Robert Harper |
| 2004 | ICALP | Self-Adjusting Computation. | Robert Harper |
| 2004 | ICASSP | Self-adjusting beat detection and prediction in music. | Robert Harper, M. Ed Jernigan |
| 2004 | LICS | Self-Adjusting Computation. | Robert Harper |
| 2004 | LICS | A Symmetric Modal Lambda Calculus for Distributed Computing. | Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning |
| 2004 | SODA | Dynamizing static algorithms, with applications to dynamic trees and history independence. | Umut A. Acar, Guy E. Blelloch, Robert Harper, Jorge L. Vittes, Shan Leung Maverick Woo |
| 2003 | ICFP | An effective theory of type refinements. | Yitzhak Mandelbaum, David Walker, Robert Harper |
| 2003 | POPL | Selective memoization. | Umut A. Acar, Guy E. Blelloch, Robert Harper |
| 2003 | POPL | A type system for higher-order modules. | Derek Dreyer, Karl Crary, Robert Harper |
| 2003 | POPL | A type theory for memory allocation and data layout. | Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning |
| 2002 | POPL | Adaptive functional programming. | Umut A. Acar, Guy E. Blelloch, Robert Harper |
| 2001 | ICFP | Automatic Generation of Staged Geometric Predicates. | Aleksandar Nanevski, Guy E. Blelloch, Robert Harper |
| 2001 | ICFP | A Dependently Typed Assembly Language. | Hongwei Xi, Robert Harper |
| 2000 | ICFP | Advanced module systems: a guide for the perplexed (abstract of invited talk). | Robert Harper, Benjamin C. Pierce |
| 2000 | POPL | Deciding Type Equivalence with Singleton Kinds. | Christopher A. Stone, Robert Harper |
| 1999 | PLDI | What is a Recursive Module? | Karl Crary, Robert Harper, Sidd Puri |
| 1998 | PLDI | Generational Stack Collection and Profile-Driven Pretenuring. | Perry Cheng, Robert Harper, Peter Lee |
| 1996 | PLDI | TIL: A Type-Directed Optimizing Compiler for ML. | David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee |
| 1996 | PLDI | TIL: a type-directed, optimizing compiler for ML (with retrospective) | David Tarditi, J. Gregory Morrisett, Perry Cheng, Christopher A. Stone, Robert Harper, Peter Lee |
| 1996 | POPL | Typed Closure Conversion. | Yasuhiko Minamide, J. Gregory Morrisett, Robert Harper |
| 1995 | POPL | Compiling Polymorphism Using Intensional Type Analysis. | Robert Harper, J. Gregory Morrisett |
| 1994 | POPL | A Type-Theoretic Approach to Higher-Order Modules with Sharing. | Robert Harper, Mark Lillibridge |
| 1993 | POPL | Explicit Polymorphism and CPS Conversion. | Robert Harper, Mark Lillibridge |
| 1991 | POPL | Typing First-Class Continuations in ML. | Bruce F. Duba, Robert Harper, David B. MacQueen |
| 1991 | POPL | A Record Calculus Based on Symmetric Concatenation. | Robert Harper, Benjamin C. Pierce |
| 1990 | POPL | Higher-Order Modules and the Phase Distinction. | Robert Harper, John C. Mitchell, Eugenio Moggi |
| 1989 | LICS | Structure and Representation in LF | Robert Harper, Donald Sannella, Andrzej Tarlecki |
| 1988 | POPL | The Essence of ML. | John C. Mitchell, Robert Harper |
| 1987 | LICS | A Framework for Defining Logics | Robert Harper, Furio Honsell, Gordon D. Plotkin |