Publications by Robert Harper

Preprint

Abstraction Functions as Types

2025
Grodin H, Li R, Harper R

Preprint

Amortized Analysis via Coalgebra

2024 • Electronic Notes in Theoretical Informatics and Computer Science • 4:11
Grodin H, Harper R

Preprint

Cost-sensitive computational adequacy of higher-order recursion in
synthetic domain theory

2024 • Electronic Notes in Theoretical Informatics and Computer Science • 4:11
Niu Y, Sterling J, Harper R

Journal Article

Decalf: A Directed, Effectful Cost-Aware Logical Framework

2024 • Proceedings of the ACM on Programming Languages • 8(POPL):
Grodin H, Niu Y, Sterling J, Harper R

Conference

A metalanguage for cost-aware denotational semantics

2023 • Proceedings - Symposium on Logic in Computer Science
Niu Y, Harper R

Preprint

A Verified Cost Analysis of Joinable Red-Black Trees

2023
Li R, Grodin H, Harper R

Preprint

Amortized Analysis via Coinduction

2023
Grodin H, Harper R

Conference

Amortized Analysis via Coinduction

2023 • Leibniz International Proceedings in Informatics • 270:
Grodin H, Harper R

Preprint

Decalf: A Directed, Effectful Cost-Aware Logical Framework

2023
Grodin H, Niu Y, Sterling J, Harper R

Preprint

Logical Relations for Session-Typed Concurrency

2023
Balzer S, Derakhshan F, Harper R, Yao Y

Journal Article

A Cost-Aware Logical Framework

2022 • Proceedings of the ACM on Programming Languages • 6:
Niu Y, Sterling J, Grodin H, Harper R

Preprint

A metalanguage for cost-aware denotational semantics

2022
Niu Y, Harper R

Conference

Sheaf Semantics of Termination-Insensitive Noninterference

2022 • Leibniz International Proceedings in Informatics • 228:
Sterling J, Harper R

Preprint

A cost-aware logical framework

2021
Niu Y, Sterling J, Grodin H, Harper R

Journal Article

An Equational Logical Framework for Type Theories

2021
Harper R

Journal Article

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

2021 • Journal of the ACM • 68(6):
Sterling J, Harper R

Journal Article

Syntax and models of Cartesian cubical type theory

2021 • Mathematical Structures in Computer Science • 31(4):424-468
Angiuli C, Brunerie G, Coquand T, Harper R, Hou (favonia) K-B, Licata DR

Journal Article

Cost-Aware Type Theory

2020
Niu Y, Harper R

Preprint

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

2020
Sterling J, Harper R

Journal Article

The History of Standard ML

2020 • Proceedings of the ACM on Programming Languages • 4:
MacQueen D, Harper R, Reppy J

Journal Article

A Separation Logic for Concurrent Randomized Programs

2019 • Proceedings of the ACM on Programming Languages • 3:
Tassarotti J, Harper R

Journal Article

Higher Inductive Types in Cubical Computational Type Theory

2019 • Proceedings of the ACM on Programming Languages • 3:
Cavallo E, Harper R

Preprint

A Separation Logic for Concurrent Randomized Programs

2018
Tassarotti J, Harper R

Conference

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities

2018 • Leibniz International Proceedings in Informatics • 119:
Angiuli C, Hou (Favonia) K-B, Harper R

Journal Article

Competitive Parallelism: Getting Your Priorities Right

2018 • Proceedings of the ACM on Programming Languages • 2:
Muller SK, Acar UA, Harper R

At a Glance

Academic Offerings

Admissions

Directory Submenu

People

Explore the Field

Publications by Robert Harper

Preprint

Preprint

Preprint

Journal Article

Conference

Preprint

Preprint

Conference

Preprint

Preprint

Journal Article

Preprint

Conference

Preprint

Journal Article

Journal Article

Journal Article

Journal Article

Preprint

Journal Article

Journal Article

Journal Article

Preprint

Conference

Journal Article

At a Glance

Academic Offerings

Admissions

Directory Submenu

People

Explore the Field

What can we help you find?

Preprint

Preprint

Preprint

Journal Article

Conference

Preprint

Preprint

Conference

Preprint

Preprint

Journal Article

Preprint

Conference

Preprint

Journal Article

Journal Article

Journal Article

Journal Article

Preprint

Journal Article

Journal Article

Journal Article

Preprint

Conference

Journal Article