Modules and Persistence in Standard ML. - Robert Harper 001 (Data Types and Persistence (Appin), 1985)

Aspects of the Implementation of Type Theory. - Robert Harper 001 (1985)

Implementing mathematics with the Nuprl proof development system. - Robert L. Constable; Stuart F. Allen; Mark Bromley; Rance Cleaveland; J. F. Cremer; Robert Harper 001; Douglas J. Howe; Todd B. Knoblock; Nax Paul Mendler; Prakash Panangaden; James T. Sasaki; Scott F. Smith 001 (Prentice Hall, 1986)

A Type Discipline for Program Modules. - Robert Harper 001; Robin Milner; Mads Tofte (TAPSOFT, Vol.2, 1987)

The Essence of ML. - John C. Mitchell; Robert Harper 001 (POPL, 1988)

Logic Representation in LF. - Robert Harper 001; Donald Sannella; Andrzej Tarlecki (Category Theory and Computer Science, 1989)

Structure and Representation in LF - Robert Harper 001; Donald Sannella; Andrzej Tarlecki (LICS, 1989)

Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft). - Robert Harper 001; Robert Pollack (TAPSOFT, Vol.2, 1989)

Definition of standard ML. - Robin Milner; Mads Tofte; Robert Harper 001 (MIT Press, 1990)

Higher-Order Modules and the Phase Distinction. - Robert Harper 001; John C. Mitchell; Eugenio Moggi (POPL, 1990)

A Record Calculus Based on Symmetric Concatenation. - Robert Harper 001; Benjamin C. Pierce (POPL, 1991)

Type Checking with Universes. - Robert Harper 001; Robert Pollack (Theor. Comput. Sci., 1991)

Constructing Type Systems over an Operational Semantics. - Robert Harper 001 (J. Symb. Comput., 1992)

Explicit Polymorphism and CPS Conversion. - Robert Harper 001; Mark Lillibridge (POPL, 1993)

A Framework for Defining Logics. - Robert Harper 001; Furio Honsell; Gordon D. Plotkin (J. ACM, 1993)

Typing First-Class Continuations in ML. - Robert Harper 001; Bruce F. Duba; David B. MacQueen (J. Funct. Program., 1993)

Polymorphic Type Assignment and CPS Conversion. - Robert Harper 001; Mark Lillibridge (LISP Symb. Comput., 1993)

On the Type Structure of Standard ML. - Robert Harper 001; John C. Mitchell (ACM Trans. Program. Lang. Syst., 1993)

Signatures for a Network Protocol Stack: A Systems Application of Standard ML. - Edoardo Biagioni; Robert Harper 001; Peter Lee 001; Brian Milnes (LISP and Functional Programming, 1994)

A Type-Theoretic Approach to Higher-Order Modules with Sharing. - Robert Harper 001; Mark Lillibridge (POPL, 1994)

Structured Theory Presentations and Logic Representations. - Robert Harper 001; Donald Sannella; Andrzej Tarlecki (Ann. Pure Appl. Log., 1994)

A Simplified Account of Polymorphic References. - Robert Harper 001 (Inf. Process. Lett., 1994)

Abstract Models of Memory Management. - J. Gregory Morrisett; Matthias Felleisen; Robert Harper 001 (FPCA, 1995)

Compiling Polymorphism Using Intensional Type Analysis. - Robert Harper 001; J. Gregory Morrisett (POPL, 1995)

TIL: A Type-Directed Optimizing Compiler for ML. - David Tarditi; J. Gregory Morrisett; Perry Cheng; Christopher A. Stone; Robert Harper 001; Peter Lee 001 (PLDI, 1996)

TIL: a type-directed, optimizing compiler for ML (with retrospective) - David Tarditi; J. Gregory Morrisett; Perry Cheng; Christopher A. Stone; Robert Harper 001; Peter Lee 001 (Best of PLDI, 1996)

Typed Closure Conversion. - Yasuhiko Minamide; J. Gregory Morrisett; Robert Harper 001 (POPL, 1996)

Research in Programming Languages for Composability, Safety, and Performance. - Robert Harper 001; Peter Lee 001 (ACM Comput. Surv., 1996)

ML and Beyond. - Robert Harper 001; John C. Mitchell (ACM Comput. Surv., 1996)

A Note on "A Simplified Account of Polymorphic References". - Robert Harper 001 (Inf. Process. Lett., 1996)

Operational Interpretations of an Extension of Fomega with Control Operators. - Robert Harper 001; Mark Lillibridge (J. Funct. Program., 1996)

Relational Interpretations of Recursive Types in an operational Setting (Summary). - Lars Birkedal; Robert Harper 001 (TACS, 1997)

Typed Closure Conversion for Recursively-Defined Functions. - J. Gregory Morrisett; Robert Harper 001 (HOOTS, 1997)

Generational Stack Collection and Profile-Driven Pretenuring. - Perry Cheng; Robert Harper 001; Peter Lee 001 (PLDI, 1998)

How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler. - Andrew Bernard; Robert Harper 001; Peter Lee 001 (Types in Compilation, 1998)

A Module System for a Programming Language Based on the LF Logical Framework. - Robert Harper 001; Frank Pfenning (J. Log. Comput., 1998)

What is a Recursive Module? - Karl Crary; Robert Harper 001; Sidd Puri (PLDI, 1999)

Relational Interpretations of Recursive Types in an Operational Setting. - Lars Birkedal; Robert Harper 001 (Inf. Comput., 1999)

Parametricity and Variants of Girard's J Operator. - Robert Harper 001; John C. Mitchell (Inf. Process. Lett., 1999)

Proof-Directed Debugging. - Robert Harper 001 (J. Funct. Program., 1999)

A type-theoretic interpretation of standard ML. - Robert Harper 001; Christopher A. Stone (Proof, Language, and Interaction, 2000)

Advanced module systems: a guide for the perplexed (abstract of invited talk). - Robert Harper 001; Benjamin C. Pierce (ICFP, 2000)

Deciding Type Equivalence with Singleton Kinds. - Christopher A. Stone; Robert Harper 001 (POPL, 2000)

A Language-Based Approach to Security. - Fred B. Schneider; J. Gregory Morrisett; Robert Harper 001 (Informatics, 2001)

A Dependently Typed Assembly Language. - Hongwei Xi 001; Robert Harper 001 (ICFP, 2001)

On the unusual effectiveness of logic in computer science. - Joseph Y. Halpern; Robert Harper 001; Neil Immerman; Phokion G. Kolaitis; Moshe Y. Vardi; Victor Vianu (Bull. Symb. Log., 2001)

Persistent triangulations Journal of Functional Programming. - Guy E. Blelloch; Hal Burch; Karl Crary; Robert Harper 001; Gary L. Miller; Noel Walkington (J. Funct. Program., 2001)

A Network Protocol Stack in Standard ML. - Edoardo Biagioni; Robert Harper 001; Peter Lee 001 (High. Order Symb. Comput., 2001)

Trustless Grid Computing in ConCert. - Bor-Yuh Evan Chang; Karl Crary; Margaret DeLap; Robert Harper 001; Jason Liszka; Tom Murphy VII; Frank Pfenning (GRID, 2002)

An effective theory of type refinements. - Yitzhak Mandelbaum; David Walker 001; Robert Harper 001 (ICFP, 2003)

Selective memoization. - Umut A. Acar; Guy E. Blelloch; Robert Harper 001 (POPL, 2003)

A type system for higher-order modules. - Derek Dreyer; Karl Crary; Robert Harper 001 (POPL, 2003)

A type theory for memory allocation and data layout. - Leaf Petersen; Robert Harper 001; Karl Crary; Frank Pfenning (POPL, 2003)

Typed compilation of recursive datatypes. - Joseph Vanderwaart; Derek Dreyer; Leaf Petersen; Karl Crary; Robert Harper 001; Perry Cheng (TLDI, 2003)

Automatic Generation of Staged Geometric Predicates. - Aleksandar Nanevski; Guy E. Blelloch; Robert Harper 001 (High. Order Symb. Comput., 2003)

Automated techniques for provably safe mobile code. - Christopher Colby; Karl Crary; Robert Harper 001; Peter Lee 001; Frank Pfenning (Theor. Comput. Sci., 2003)

Self-adjusting beat detection and prediction in music. - Robert Harper 001; M. Ed Jernigan (ICASSP (4), 2004)

Self-Adjusting Computation. - Robert Harper 001 (LICS, 2004)

A Symmetric Modal Lambda Calculus for Distributed Computing. - Tom Murphy VII; Karl Crary; Robert Harper 001; Frank Pfenning (LICS, 2004)

Dynamizing static algorithms, with applications to dynamic trees and history independence. - Umut A. Acar; Guy E. Blelloch; Robert Harper 001; Jorge L. Vittes; Shan Leung Maverick Woo (SODA, 2004)

Editorial. - David A. Basin; Olivier Danvy; Robert Harper 001 (High. Order Symb. Comput., 2004)

Distributed Control Flow with Classical Modal Logic. - Tom Murphy VII; Karl Crary; Robert Harper 001 (CSL, 2005)

Mechanizing the meta-theory of programming languages. - Robert Harper 001 (ICFP, 2005)

Strict bidirectional type checking. - Adam Chlipala; Leaf Petersen; Robert Harper 001 (TLDI, 2005)

Using page residency to balance tradeoffs in tracing garbage collection. - Daniel Spoonhower; Guy E. Blelloch; Robert Harper 001 (VEE, 2005)

A Library for Self-Adjusting Computation. - Umut A. Acar; Guy E. Blelloch; Matthias Blume; Robert Harper 001; Kanat Tangwongsan (ML, 2005)

On equivalence and canonical forms in the LF type theory. - Robert Harper 001; Frank Pfenning (ACM Trans. Comput. Log., 2005)

A separate compilation extension to standard ML. - David Swasey; Tom Murphy VII; Karl Crary; Robert Harper 001 (ML, 2006)

Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight - Karl Crary; Robert Harper 001 (CoRR, 2006)

Higher-order abstract syntax: setting the record straight. - Karl Crary; Robert Harper 001 (SIGACT News, 2006)

Extensional equivalence and singleton types. - Christopher A. Stone; Robert Harper 001 (ACM Trans. Comput. Log., 2006)

Adaptive functional programming. - Umut A. Acar; Guy E. Blelloch; Robert Harper 001 (ACM Trans. Program. Lang. Syst., 2006)

Modular type classes. - Derek Dreyer; Robert Harper 001; Manuel M. T. Chakravarty; Gabriele Keller (POPL, 2007)

Towards a mechanized metatheory of standard ML. - Daniel K. Lee; Karl Crary; Robert Harper 001 (POPL, 2007)

Type-Safe Distributed Programming with ML5. - Tom Murphy VII; Karl Crary; Robert Harper 001 (TGC, 2007)

Syntactic Logical Relations for Polymorphic and Recursive Types. - Karl Crary; Robert Harper 001 (Computation, Meaning, and Logic, 2007)

Mechanizing metatheory in a logical framework. - Robert Harper 001; Daniel R. Licata (J. Funct. Program., 2007)

Focusing on Binding and Computation. - Daniel R. Licata; Noam Zeilberger; Robert Harper 001 (LICS, 2008)

SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations. - Eric Allen; Mark W. Bailey; Rastislav Bodík; Kim B. Bruce; Kathleen Fisher; Stephen N. Freund; Robert Harper 001; Chandra Krintz; Shriram Krishnamurthi; James R. Larus; Doug Lea; Gary T. Leavens; et al. (ACM SIGPLAN Notices, 2008)

Position paper: practical foundations for lrogramming languages. - Robert Harper 001 (ACM SIGPLAN Notices, 2008)

A universe of binding and computation. - Daniel R. Licata; Robert Harper 001 (ICFP, 2009)

Positively dependent types. - Daniel R. Licata; Robert Harper 001 (PLPV, 2009)

Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report. - Mark W. Bailey; Kim B. Bruce; Kathleen Fisher; Robert Harper 001; Stuart Reges (SIGCSE, 2009)

Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures. - Daniel Spoonhower; Guy E. Blelloch; Phillip B. Gibbons; Robert Harper 001 (SPAA, 2009)

A Pronominal Approach to Binding and Computation. - Robert Harper 001; Daniel R. Licata; Noam Zeilberger (TLCA, 2009)

FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum. - Robert Harper 001 (J. Funct. Program., 2009)

An overview of the Oregon programming languages summer school. - Jim Allen; Zena M. Ariola; Pierre-Louis Curien; Matthew Fluet; Jeffrey S. Foster; Dan Grossman; Robert Harper 001; Hugo Herbelin; Yannis Smaragdakis; David Walker 001; Steve Zdancewic (ACM SIGPLAN Notices, 2009)

An experimental analysis of self-adjusting computation. - Umut A. Acar; Guy E. Blelloch; Matthias Blume; Robert Harper 001; Kanat Tangwongsan (ACM Trans. Program. Lang. Syst., 2009)

Distributed programming with distributed authorization. - Kumar Avijit; Anupam Datta; Robert Harper 001 (TLDI, 2010)

A Monadic Formalization of ML5 - Daniel R. Licata; Robert Harper 001 (LFMTP, 2010)

Space profiling for parallel functional programs. - Daniel Spoonhower; Guy E. Blelloch; Robert Harper 001; Phillip B. Gibbons (J. Funct. Program., 2010)

Robin Milner 1934–2010: verification, languages, and concurrency. - Andrew D. Gordon 001; Robert Harper 001; John Harrison 001; Alan Jeffrey; Peter Sewell (POPL, 2011)

2-Dimensional Directed Type Theory. - Daniel R. Licata; Robert Harper 001 (MFPS, 2011)

Canonicity for 2-dimensional type theory. - Daniel R. Licata; Robert Harper 001 (POPL, 2012)

Cache and I/O efficent functional algorithms. - Guy E. Blelloch; Robert Harper 001 (POPL, 2013)

Cache efficient functional algorithms. - Guy E. Blelloch; Robert Harper 001 (Commun. ACM, 2015)

A Note on the Uniform Kan Condition in Nominal Cubical Sets. - Robert Harper 001; Kuen-Bang Hou (Favonia) (CoRR, 2015)

Homotopy type theory: unified foundations of mathematics and computation. - Steve Awodey; Robert Harper 001 (ACM SIGLOG News, 2015)

Practical Foundations for Programming Languages (2nd. Ed.). - Robert Harper 001 (Cambridge University Press, 2016)

Covering Spaces in Homotopy Type Theory. - Kuen-Bang Hou (Favonia); Robert Harper 001 (TYPES, 2016)

Computational Higher Type Theory I: Abstract Cubical Realizability. - Carlo Angiuli; Robert Harper 001; Todd Wilson (CoRR, 2016)

Computational Higher Type Theory II: Dependent Cubical Realizability. - Carlo Angiuli; Robert Harper 001 (CoRR, 2016)

Homotopical patch theory. - Carlo Angiuli; Edward Morehouse; Daniel R. Licata; Robert Harper 001 (J. Funct. Program., 2016)

A Higher-Order Logic for Concurrent Termination-Preserving Refinement. - Joseph Tassarotti; Ralf Jung 002; Robert Harper 001 (ESOP, 2017)

Responsive parallel computation: bridging competitive and cooperative threading. - Stefan K. Muller; Umut A. Acar; Robert Harper 001 (PLDI, 2017)

Computational higher-dimensional type theory. - Carlo Angiuli; Robert Harper 001; Todd Wilson (POPL, 2017)

Parallel functional arrays. - Ananya Kumar; Guy E. Blelloch; Robert Harper 001 (POPL, 2017)

Algebraic Foundations of Proof Refinement. - Jonathan Sterling; Robert Harper 001 (CoRR, 2017)

Computational Higher Type Theory III: Univalent Universes and Exact Equality. - Carlo Angiuli; Kuen-Bang Hou (Favonia); Robert Harper 001 (CoRR, 2017)

Correctness of compiling polymorphism to dynamic typing. - Kuen-Bang Hou (Favonia); Nick Benton; Robert Harper 001 (J. Funct. Program., 2017)

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. - Carlo Angiuli; Kuen-Bang Hou (Favonia); Robert Harper 001 (CSL, 2018)

Verified Tail Bounds for Randomized Programs. - Joseph Tassarotti; Robert Harper 001 (ITP, 2018)

Guarded Computational Type Theory. - Jonathan Sterling; Robert Harper 001 (LICS, 2018)

Computational Higher Type Theory IV: Inductive Types. - Evan Cavallo; Robert Harper 001 (CoRR, 2018)

The RedPRL Proof Assistant (Invited Paper). - Carlo Angiuli; Evan Cavallo; Kuen-Bang Hou (Favonia); Robert Harper 001; Jonathan Sterling (LFMTP@FSCD, 2018)

Competitive parallelism: getting your priorities right. - Stefan K. Muller; Umut A. Acar; Robert Harper 001 (Proc. ACM Program. Lang., 2018)

Exception tracking in an open world. - Robert Harper 001 (Theor. Comput. Sci., 2018)

Parametric Cubical Type Theory. - Evan Cavallo; Robert Harper 001 (CoRR, 2019)

Higher inductive types in cubical computational type theory. - Evan Cavallo; Robert Harper 001 (Proc. ACM Program. Lang., 2019)

A separation logic for concurrent randomized programs. - Joseph Tassarotti; Robert Harper 001 (Proc. ACM Program. Lang., 2019)

Cost-Aware Type Theory. - Yue Niu; Robert Harper 001 (CoRR, 2020)

The history of Standard ML. - David MacQueen; Robert Harper 001; John H. Reppy (Proc. ACM Program. Lang., 2020)

An Equational Logical Framework for Type Theories. - Robert Harper 001 (CoRR, 2021)

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. - Jonathan Sterling; Robert Harper 001 (J. ACM, 2021)

Internal Parametricity for Cubical Type Theory. - Evan Cavallo; Robert Harper 001 (Log. Methods Comput. Sci., 2021)

Syntax and models of Cartesian cubical type theory. - Carlo Angiuli; Guillaume Brunerie; Thierry Coquand; Robert Harper 001; Kuen-Bang Hou (Favonia); Daniel R. Licata (Math. Struct. Comput. Sci., 2021)

Sheaf Semantics of Termination-Insensitive Noninterference. - Jonathan Sterling; Robert Harper 001 (FSCD, 2022)

A cost-aware logical framework. - Yue Niu; Jonathan Sterling; Harrison Grodin; Robert Harper 001 (Proc. ACM Program. Lang., 2022)

Integrating Cost and Behavior in Type Theory (Invited Talk). - Robert Harper 001 (CALCO, 2023)

Amortized Analysis via Coinduction (Early Ideas). - Harrison Grodin; Robert Harper 001 (CALCO, 2023)

A Metalanguage for Cost-Aware Denotational Semantics. - Yue Niu; Robert Harper 001 (LICS, 2023)

Amortized Analysis via Coinduction. - Harrison Grodin; Robert Harper 001 (CoRR, 2023)

Logical Relations for Session-Typed Concurrency. - Stephanie Balzer; Farzaneh Derakhshan; Robert Harper 001; Yue Yao (CoRR, 2023)

A Verified Cost Analysis of Joinable Red-Black Trees. - Runming Li; Harrison Grodin; Robert Harper 001 (CoRR, 2023)

Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. - Yue Niu; Jonathan Sterling; Robert Harper 001 (CoRR, 2024)

Amortized Analysis via Coalgebra. - Harrison Grodin; Robert Harper 001 (CoRR, 2024)

Decalf: A Directed, Effectful Cost-Aware Logical Framework. - Harrison Grodin; Yue Niu; Jonathan Sterling; Robert Harper 001 (Proc. ACM Program. Lang., 2024)

Abstraction Functions as Types. - Harrison Grodin; Runming Li; Robert Harper 001 (CoRR, 2025)

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. - Runming Li; Robert Harper 001 (CoRR, 2025)