Robert Harper

ORCID

Publication Activity (10 Years)

Years Active: 1985-2024
Publications (10 Years): 49

Top Venues

CoRR

Proc. ACM Program. Lang.

CALCO

POPL

Publications

Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper
Decalf: A Directed, Effectful Cost-Aware Logical Framework. Proc. ACM Program. Lang. 8 (POPL) (2024)
Harrison Grodin, Robert Harper
Amortized Analysis via Coalgebra. CoRR (2024)
Yue Niu, Jonathan Sterling, Robert Harper
Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. CoRR (2024)
Yue Niu, Robert Harper
A Metalanguage for Cost-Aware Denotational Semantics. LICS (2023)
Harrison Grodin, Robert Harper
Amortized Analysis via Coinduction. CoRR (2023)
Harrison Grodin, Robert Harper
Amortized Analysis via Coinduction (Early Ideas). CALCO (2023)
Robert Harper
Integrating Cost and Behavior in Type Theory (Invited Talk). CALCO (2023)
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao
Logical Relations for Session-Typed Concurrency. CoRR (2023)
Harrison Grodin, Robert Harper, Yue Niu, Jonathan Sterling
Decalf: A Directed, Effectful Cost-Aware Logical Framework. CoRR (2023)
Runming Li, Harrison Grodin, Robert Harper
A Verified Cost Analysis of Joinable Red-Black Trees. CoRR (2023)
Jonathan Sterling, Robert Harper
Sheaf semantics of termination-insensitive noninterference. CoRR (2022)
Yue Niu, Robert Harper
A metalanguage for cost-aware denotational semantics. CoRR (2022)
Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper
A cost-aware logical framework. Proc. ACM Program. Lang. 6 (POPL) (2022)
Jonathan Sterling, Robert Harper
Sheaf Semantics of Termination-Insensitive Noninterference. FSCD (2022)
Robert Harper
An Equational Logical Framework for Type Theories. CoRR (2021)
Jonathan Sterling, Robert Harper
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM 68 (6) (2021)
Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper
A cost-aware logical framework. CoRR (2021)
Evan Cavallo, Robert Harper
Internal Parametricity for Cubical Type Theory. Log. Methods Comput. Sci. 17 (4) (2021)
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. 31 (4) (2021)
Jonathan Sterling, Robert Harper
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. CoRR (2020)
Evan Cavallo, Robert Harper
Internal Parametricity for Cubical Type Theory. CoRR (2020)
Evan Cavallo, Robert Harper
Internal Parametricity for Cubical Type Theory. CSL (2020)
Yue Niu, Robert Harper
Cost-Aware Type Theory. CoRR (2020)
David MacQueen, Robert Harper, John H. Reppy
The history of Standard ML. Proc. ACM Program. Lang. 4 (HOPL) (2020)
Joseph Tassarotti, Robert Harper
A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3 (POPL) (2019)
Evan Cavallo, Robert Harper
Higher inductive types in cubical computational type theory. Proc. ACM Program. Lang. 3 (POPL) (2019)
Evan Cavallo, Robert Harper
Parametric Cubical Type Theory. CoRR (2019)
Jonathan Sterling, Robert Harper
Guarded Computational Type Theory. CoRR (2018)
Joseph Tassarotti, Robert Harper
Verified Tail Bounds for Randomized Programs. ITP (2018)
Stefan K. Muller, Umut A. Acar, Robert Harper
Competitive Parallelism: Getting Your Priorities Right. CoRR (2018)
Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. CSL (2018)
Joseph Tassarotti, Robert Harper
A Separation Logic for Concurrent Randomized Programs. CoRR (2018)
Stefan K. Muller, Umut A. Acar, Robert Harper
Competitive parallelism: getting your priorities right. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou, Robert Harper, Jonathan Sterling
The RedPRL Proof Assistant (Invited Paper). LFMTP@FSCD (2018)
Evan Cavallo, Robert Harper
Computational Higher Type Theory IV: Inductive Types. CoRR (2018)
Robert Harper
Exception tracking in an open world. Theor. Comput. Sci. 741 (2018)
Jonathan Sterling, Robert Harper
Guarded Computational Type Theory. LICS (2018)
Kuen-Bang Hou (Favonia), Nick Benton, Robert Harper
Correctness of compiling polymorphism to dynamic typing. J. Funct. Program. 27 (2017)
Jonathan Sterling, Robert Harper
Algebraic Foundations of Proof Refinement. CoRR (2017)
Stefan K. Muller, Umut A. Acar, Robert Harper
Responsive parallel computation: bridging competitive and cooperative threading. PLDI (2017)
Joseph Tassarotti, Ralf Jung, Robert Harper
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. ESOP (2017)
Carlo Angiuli, Kuen-Bang Hou, Robert Harper
Computational Higher Type Theory III: Univalent Universes and Exact Equality. CoRR (2017)
Carlo Angiuli, Robert Harper, Todd Wilson
Computational higher-dimensional type theory. POPL (2017)
Joseph Tassarotti, Ralf Jung, Robert Harper
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. CoRR (2017)
Ananya Kumar, Guy E. Blelloch, Robert Harper
Parallel functional arrays. POPL (2017)
Carlo Angiuli, Robert Harper
Computational Higher Type Theory II: Dependent Cubical Realizability. CoRR (2016)
Kuen-Bang Hou (Favonia), Robert Harper
Covering Spaces in Homotopy Type Theory. TYPES (2016)
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
Homotopical patch theory. J. Funct. Program. 26 (2016)
Carlo Angiuli, Robert Harper, Todd Wilson
Computational Higher Type Theory I: Abstract Cubical Realizability. CoRR (2016)
Steve Awodey, Robert Harper
Homotopy type theory: unified foundations of mathematics and computation. ACM SIGLOG News 2 (1) (2015)
Robert Harper, Kuen-Bang Hou
A Note on the Uniform Kan Condition in Nominal Cubical Sets. CoRR (2015)
Guy E. Blelloch, Robert Harper
Cache efficient functional algorithms. Commun. ACM 58 (7) (2015)
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
Homotopical patch theory. ICFP (2014)
Guy E. Blelloch, Robert Harper
Cache and I/O efficent functional algorithms. POPL (2013)
Daniel R. Licata, Robert Harper
Canonicity for 2-dimensional type theory. POPL (2012)
Umut A. Acar, Guy E. Blelloch, Robert Harper
Selective Memoization CoRR (2011)
Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell
Robin Milner 1934--2010: verification, languages, and concurrency. POPL (2011)
Daniel R. Licata, Robert Harper
2-Dimensional Directed Type Theory. MFPS (2011)
Daniel R. Licata, Robert Harper
A Monadic Formalization of ML5 LFMTP (2010)
Kumar Avijit, Anupam Datta, Robert Harper
Distributed programming with distributed authorization. TLDI (2010)
Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons
Space profiling for parallel functional programs. J. Funct. Program. 20 (5-6) (2010)
Jim Allen, Zena M. Ariola, Pierre-Louis Curien, Matthew Fluet, Jeffrey S. Foster, Dan Grossman, Robert Harper, Hugo Herbelin, Yannis Smaragdakis, David Walker, Steve Zdancewic
An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 44 (11) (2009)
Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan
An experimental analysis of self-adjusting computation. ACM Trans. Program. Lang. Syst. 32 (1) (2009)
Daniel R. Licata, Robert Harper
A universe of binding and computation. ICFP (2009)
Daniel Spoonhower, Guy E. Blelloch, Phillip B. Gibbons, Robert Harper
Beyond nested parallelism: tight bounds on work-stealing overheads for parallel futures. SPAA (2009)
Robert Harper, Daniel R. Licata, Noam Zeilberger
A Pronominal Approach to Binding and Computation. TLCA (2009)
Daniel R. Licata, Robert Harper
Positively dependent types. PLPV (2009)
Robert Harper
FUNCTIONAL PEARL. Proof-directed debugging - Corrigendum. J. Funct. Program. 19 (2) (2009)
Mark W. Bailey, Kim B. Bruce, Kathleen Fisher, Robert Harper, Stuart Reges
Report of the 2008 SIGPLAN programming languages curriculum workshop: preliminary report. SIGCSE (2009)
Robert Harper
Position paper: practical foundations for lrogramming languages. ACM SIGPLAN Notices 43 (11) (2008)
Eric Allen, Mark W. Bailey, Rastislav Bodík, Kim B. Bruce, Kathleen Fisher, Stephen N. Freund, Robert Harper, Chandra Krintz, Shriram Krishnamurthi, James R. Larus, Doug Lea, Gary T. Leavens, Lori L. Pollock, Stuart Reges, Martin C. Rinard, Mark A. Sheldon, Franklyn A. Turbak, Mitchell Wand
SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations. ACM SIGPLAN Notices 43 (11) (2008)
Daniel R. Licata, Noam Zeilberger, Robert Harper
Focusing on Binding and Computation. LICS (2008)
Daniel Spoonhower, Guy E. Blelloch, Robert Harper, Phillip B. Gibbons
Space profiling for parallel functional programs. ICFP (2008)
Robert Harper, Daniel R. Licata
Mechanizing metatheory in a logical framework. J. Funct. Program. 17 (4-5) (2007)
Karl Crary, Robert Harper
Syntactic Logical Relations for Polymorphic and Recursive Types. Electron. Notes Theor. Comput. Sci. 172 (2007)
Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller
Modular type classes. POPL (2007)
Tom Murphy VII, Karl Crary, Robert Harper
Type-Safe Distributed Programming with ML5. TGC (2007)
Daniel K. Lee, Karl Crary, Robert Harper
Towards a mechanized metatheory of standard ML. POPL (2007)
Karl Crary, Robert Harper
Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight CoRR (2006)
Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan
A Library for Self-Adjusting Computation. Electron. Notes Theor. Comput. Sci. 148 (2) (2006)
Umut A. Acar, Guy E. Blelloch, Robert Harper
Adaptive functional programming. ACM Trans. Program. Lang. Syst. 28 (6) (2006)
David Swasey, Tom Murphy VII, Karl Crary, Robert Harper
A separate compilation extension to standard ML. ML (2006)
Karl Crary, Robert Harper
Higher-order abstract syntax: setting the record straight. SIGACT News 37 (3) (2006)
Christopher A. Stone, Robert Harper
Extensional equivalence and singleton types. ACM Trans. Comput. Log. 7 (4) (2006)
Daniel Spoonhower, Guy E. Blelloch, Robert Harper
Using page residency to balance tradeoffs in tracing garbage collection. VEE (2005)
Robert Harper
Mechanizing the meta-theory of programming languages. ICFP (2005)
Adam Chlipala, Leaf Petersen, Robert Harper
Strict bidirectional type checking. TLDI (2005)
Tom Murphy VII, Karl Crary, Robert Harper
Distributed Control Flow with Classical Modal Logic. CSL (2005)
Robert Harper, Frank Pfenning
On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6 (1) (2005)
Robert Harper
Self-Adjusting Computation. ICALP (2004)
Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
A Symmetric Modal Lambda Calculus for Distributed Computing. LICS (2004)
David A. Basin, Olivier Danvy, Robert Harper
Editorial. High. Order Symb. Comput. 17 (3) (2004)
Robert Harper
Self-Adjusting Computation. LICS (2004)
Umut A. Acar, Guy E. Blelloch, Robert Harper, Jorge L. Vittes, Shan Leung Maverick Woo
Dynamizing static algorithms, with applications to dynamic trees and history independence. SODA (2004)
Robert Harper, M. Ed Jernigan
Self-adjusting beat detection and prediction in music. ICASSP (4) (2004)
Yitzhak Mandelbaum, David Walker, Robert Harper
An effective theory of type refinements. ICFP (2003)
David Walker, Robert Harper, Yitzhak Mandelbaum
An effective theory of type refinements. SIGPLAN Notices (2003)
Derek Dreyer, Karl Crary, Robert Harper
A type system for higher-order modules. POPL (2003)
Aleksandar Nanevski, Guy E. Blelloch, Robert Harper
Automatic Generation of Staged Geometric Predicates. High. Order Symb. Comput. 16 (4) (2003)
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
Automated techniques for provably safe mobile code. Theor. Comput. Sci. 290 (2) (2003)

Robert Harper.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Robert Harper