Preprint Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory 2024 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
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
Conference Sheaf Semantics of Termination-Insensitive Noninterference 2022 • Leibniz International Proceedings in Informatics • 228: Sterling J, Harper R
Conference Internal parametricity for cubical type theory 2021 • Logical Methods in Computer Science • 17(4):5:1-5:60 Cavallo E, 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
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
Conference Cartesian cubical computational type theory: Constructive reasoning with paths and equalities 2018 • Leibniz International Proceedings in Informatics • 119: Angiuli C, Hou KB, Harper R
