List of research outcomes
This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!
| Publication | Date of Publication | Type |
|---|---|---|
| Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory | 2026-04-02 | Paper |
| Amortized analysis via coalgebra | 2026-04-02 | Paper |
| Integrating cost and behavior in type theory (invited talk) | 2024-11-26 | Paper |
| Amortized analysis via coinduction (early ideas) | 2024-11-26 | Paper |
| Sheaf semantics of termination-insensitive noninterference | 2024-05-27 | Paper |
| Internal Parametricity for Cubical Type Theory | 2023-02-07 | Paper |
| Logical Relations as Types: Proof-Relevant Parametricity for Program Modules Journal of the ACM | 2022-12-08 | Paper |
| Logic representation in LF Category Theory and Computer Science | 2022-08-16 | Paper |
| Cartesian cubical computational type theory: Constructive reasoning with paths and equalities | 2022-05-28 | Paper |
| Internal parametricity for cubical type theory (available as arXiv preprint) | 2022-02-09 | Paper |
| Internal parametricity for cubical type theory | 2022-02-09 | Paper |
| Syntax and models of Cartesian cubical type theory Mathematical Structures in Computer Science | 2022-01-20 | Paper |
| An Equational Logical Framework for Type Theories | 2021-06-02 | Paper |
| Guarded computational type theory Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
| Verified tail bounds for randomized programs | 2018-10-04 | Paper |
| Exception tracking in an open world Theoretical Computer Science | 2018-07-26 | Paper |
| Meaning explanations at higher dimension Indagationes Mathematicae. New Series | 2018-01-12 | Paper |
| Correctness of compiling polymorphism to dynamic typing Journal of Functional Programming | 2017-10-23 | Paper |
| Homotopical patch theory Journal of Functional Programming | 2017-10-23 | Paper |
| Computational higher-dimensional type theory Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
| Parallel functional arrays Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
| Extensional equivalence and singleton types ACM Transactions on Computational Logic | 2017-07-12 | Paper |
| On equivalence and canonical forms in the LF type theory ACM Transactions on Computational Logic | 2017-07-12 | Paper |
| A higher-order logic for concurrent termination-preserving refinement Programming Languages and Systems | 2017-05-19 | Paper |
| Homotopical patch theory Proceedings of the 19th ACM SIGPLAN international conference on Functional programming | 2016-09-29 | Paper |
| 2-Dimensional Directed Type Theory Electronic Notes in Theoretical Computer Science | 2016-07-15 | Paper |
| Practical foundations for programming languages | 2016-05-11 | Paper |
| Canonicity for 2-dimensional type theory Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
| A type system for higher-order modules Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
| A type theory for memory allocation and data layout Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
| Dynamizing static algorithms, with applications to dynamic trees and history independence | 2015-08-03 | Paper |
| Deciding type equivalence in a language with singleton kinds Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
| Adaptive functional programming Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
| Space profiling for parallel functional programs Proceedings of the 13th ACM SIGPLAN international conference on Functional programming | 2015-03-16 | Paper |
| Automatic generation of staged geometric predicates Proceedings of the sixth ACM SIGPLAN international conference on Functional programming | 2015-03-09 | Paper |
| A dependently typed assembly language Proceedings of the sixth ACM SIGPLAN international conference on Functional programming | 2015-03-09 | Paper |
| A Note on the Uniform Kan Condition in Nominal Cubical Sets | 2015-01-22 | Paper |
| A universe of binding and computation Proceedings of the 14th ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
| Towards a mechanized metatheory of Standard ML Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
| Modular type classes Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
| Syntactic logical relations for polymorphic and recursive types Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
| Space profiling for parallel functional programs Journal of Functional Programming | 2011-07-25 | Paper |
| Mechanizing metatheory in a logical framework Journal of Functional Programming | 2007-09-26 | Paper |
| Computer Science Logic Lecture Notes in Computer Science | 2006-11-01 | Paper |
| Automata, Languages and Programming Lecture Notes in Computer Science | 2005-08-24 | Paper |
| Corrigendum: Polymorphic type assignment and CPS conversion Higher-Order and Symbolic Computation | 2004-03-15 | Paper |
| Automatic generation of staged geometric predicates Higher-Order and Symbolic Computation | 2004-03-15 | Paper |
| scientific article; zbMATH DE number 1966243 (Why is no real title available?) | 2003-08-18 | Paper |
| Relational interpretations of recursive types in an operational setting. Information and Computation | 2003-01-14 | Paper |
| Parametricity and variants of Girard's \(J\) operator Information Processing Letters | 2002-07-25 | Paper |
| Persistent triangulations Journal of Functional Programming | 2001-11-21 | Paper |
| On the unusual effectiveness of logic in computer science The Bulletin of Symbolic Logic | 2001-09-10 | Paper |
| On the unusual effectiveness of logic in computer science The Bulletin of Symbolic Logic | 2001-09-10 | Paper |
| Semantics of memory management for polymorphic languages | 2001-07-08 | Paper |
| Proof-directed debugging Journal of Functional Programming | 2000-03-16 | Paper |
| scientific article; zbMATH DE number 1231621 (Why is no real title available?) | 1999-01-06 | Paper |
| A module system for a programming language based on the LF logical framework Journal Of Logic And Computation | 1998-07-28 | Paper |
| scientific article; zbMATH DE number 1088048 (Why is no real title available?) | 1997-11-17 | Paper |
| A note on ``A simplified account of polymorphic references Information Processing Letters | 1997-02-27 | Paper |
| Operational interpretations of an extension of Fω with control operators Journal of Functional Programming | 1996-12-16 | Paper |
| Structured theory presentations and logic representations Annals of Pure and Applied Logic | 1995-03-29 | Paper |
| A simplified account of polymorphic references Information Processing Letters | 1994-09-25 | Paper |
| A framework for defining logics Journal of the ACM | 1993-05-16 | Paper |
| Constructing type systems over an operational semantics Journal of Symbolic Computation | 1993-01-16 | Paper |
| Type checking with universes Theoretical Computer Science | 1992-06-26 | Paper |
| scientific article; zbMATH DE number 4180831 (Why is no real title available?) | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 3995028 (Why is no real title available?) | 1987-01-01 | Paper |
| Amortized Analysis via Coalgebra (available as arXiv preprint) | N/A | Paper |
Research outcomes over time
This page was built for person: Robert Harper
