Journal Article Abstraction Functions as Types Modular Verification of Cost and Behavior in Dependent Type Theory 2026 • Proceedings of the ACM on Programming Languages • 10(POPL): Grodin H, Li R, Harper R
Preprint Decalf: A Directed, Effectful Cost-Aware Logical Framework 2026 Grodin H, Niu Y, Sterling J, Harper R
Preprint Logical Relations for Session-Typed Concurrency 2026 Balzer S, Derakhshan F, Harper R, Yao Y
Conference Mechanizing Synthetic Tait Computability in Istari 2026 • PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026 • 231-247 Li R, Yao Y, Harper R
Chapter Recursive Logical Relations for Intuitionistic Linear Logic Session Types 2026 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 16501:135-165 Balzer S, Derakhshan F, Harper R, Yao Y
Preprint Amortized Analysis via Coalgebra 2024 • Electronic Notes in Theoretical Informatics and Computer Science 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 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
Conference Amortized Analysis via Coinduction 2023 • Leibniz International Proceedings in Informatics • 270: Grodin H, Harper R
Journal Article A Cost-Aware Logical Framework 2022 • Proceedings of the ACM on Programming Languages • 6: Niu Y, Sterling J, Grodin H, Harper R
Conference Sheaf Semantics of Termination-Insensitive Noninterference 2022 • Leibniz International Proceedings in Informatics • 228: Sterling J, Harper R
Preprint Logical Relations as Types: Proof-Relevant Parametricity for Program Modules 2021 Sterling J, 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
