Conference A Metalanguage for Cost-Aware Denotational Semantics 2023 • Proceedings - Symposium on Logic in Computer Science • 2023-June: Niu Y, Harper R
Preprint Decalf: A Directed, Effectful Cost-Aware Logical Framework 2023 Grodin H, Harper R, Niu Y, Sterling J
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
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
Journal Article Competitive Parallelism: Getting Your Priorities Right 2018 • Proceedings of the ACM on Programming Languages • 2: Muller SK, Acar UA, Harper R
Conference Covering spaces in homotopy type theory 2018 • Leibniz International Proceedings in Informatics • 97: Favonia KBH, Harper R
Journal Article Exception tracking in an open world 2018 • Theoretical Computer Science • 741:25-31 Harper R
Conference Guarded computational type theory 2018 • Proceedings - Symposium on Logic in Computer Science • 879-888 Sterling J, Harper R
Journal Article Meaning explanations at higher dimension 2018 • Indagationes Mathematicae • 29(1):135-149 Angiuli C, Harper R
Preprint The RedPRL Proof Assistant (Invited Paper) 2018 Angiuli C, Cavallo E, Hou K-B, Harper R, Sterling J
