| Publication | Date of Publication | Type |
|---|
Amortized Analysis via Coalgebra
(available as arXiv preprint) | N/A | Paper |
| Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory | 2026-04-02 | Paper |
| Amortized analysis via coalgebra | 2026-04-02 | Paper |
| A metalanguage for cost-aware denotational semantics | 2026-02-27 | Paper |
| Covering spaces in homotopy type theory | 2026-02-20 | Paper |
| The RedPRL proof assistant (invited paper) | 2025-08-19 | Paper |
| A monadic formalization of ML5 | 2025-08-19 | 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 |
An Equational Logical Framework for Type Theories
(available as arXiv preprint) | 2021-01-01 | 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 |
Homotopical patch theory
Journal of Functional Programming | 2017-10-23 | Paper |
Correctness of compiling polymorphism to dynamic typing
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 |
On equivalence and canonical forms in the LF type theory
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Extensional equivalence and singleton types
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 theory for memory allocation and data layout
Proceedings of the 30th 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 |
| 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 |
A dependently typed assembly language
Proceedings of the sixth ACM SIGPLAN international conference on Functional programming | 2015-03-09 | Paper |
Automatic generation of staged geometric predicates
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 |
A Note on the Uniform Kan Condition in Nominal Cubical Sets
(available as arXiv preprint) | 2015-01-01 | Paper |
Modular type classes
Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | 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 |
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 |
Automatic generation of staged geometric predicates
Higher-Order and Symbolic Computation | 2004-03-15 | Paper |
Corrigendum: Polymorphic type assignment and CPS conversion
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<sub>ω</sub> 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 |
