| Publication | Date of Publication | Type |
|---|
| Patch locale of a spectral locale in univalent type theory | 2026-04-02 | Paper |
| Parametricity, automorphisms of the universe, and excluded middle | 2026-02-20 | Paper |
| Computing Nash equilibria of unbounded games | 2026-01-14 | Paper |
Continuous and algebraic domains in univalent foundations
Journal of Pure and Applied Algebra | 2025-09-29 | Paper |
The patch topology in univalent foundations
Mathematical Structures in Computer Science | 2025-09-01 | Paper |
| Type theory with explicit universe polymorphism | 2024-11-26 | Paper |
Higher-order games with dependent types
Theoretical Computer Science | 2023-09-18 | Paper |
On Small Types in Univalent Foundations
Logical Methods in Computer Science | 2023-08-26 | Paper |
Predicative Aspects of Order Theory in Univalent Foundations
(available as arXiv preprint) | 2023-06-23 | Paper |
| Kreisel's counter-example to full abstraction of the set-theoretical model of Goedel's system T | 2023-03-16 | Paper |
On generalized algebraic theories and categories with families
Mathematical Structures in Computer Science | 2022-06-24 | Paper |
Injective types in univalent mathematics
Mathematical Structures in Computer Science | 2021-10-11 | Paper |
The Cantor-Schröder-Bernstein theorem for -groupoids
Journal of Homotopy and Related Structures | 2021-09-28 | Paper |
A Note on Generalized Algebraic Theories and Categories with Families
(available as arXiv preprint) | 2020-12-15 | Paper |
| Domain Theory in Constructive and Predicative Univalent Foundations | 2020-08-04 | Paper |
| Partial elements and recursion via dominances in univalent type theory | 2020-05-26 | Paper |
The Cantor-Schr\"oder-Bernstein Theorem for $\infty$-groupoids
(available as arXiv preprint) | 2020-02-13 | Paper |
| Intersections of compactly many open sets are open | 2020-01-16 | Paper |
| Introduction to Univalent Foundations of Mathematics with Agda | 2019-11-01 | Paper |
| A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom | 2018-03-06 | Paper |
The Herbrand functional interpretation of the double negation shift
Journal of Symbolic Logic | 2017-08-03 | Paper |
| The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation | 2017-07-12 | Paper |
Notions of anonymous existence in Martin-Löf type theory
(available as arXiv preprint) | 2017-05-08 | Paper |
| Parametricity, automorphisms of the universe, and excluded middle | 2017-01-19 | Paper |
Constructive decidability of classical continuity
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
A constructive manifestation of the Kleene-Kreisel continuous functionals
Annals of Pure and Applied Logic | 2016-06-03 | Paper |
The intrinsic topology of Martin-Löf universes
Annals of Pure and Applied Logic | 2016-06-03 | Paper |
Semi-decidability of may, must and probabilistic testing in a higher-type setting
Electronic Notes in Theoretical Computer Science | 2016-05-10 | Paper |
| Continuity of Gödel's system T definable functionals via effectful forcing | 2016-04-12 | Paper |
Bar recursion and products of selection functions
Journal of Symbolic Logic | 2015-05-20 | Paper |
Abstract datatypes for real numbers in type theory
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics
The Journal of Symbolic Logic | 2014-01-07 | Paper |
Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics
The Journal of Symbolic Logic | 2014-01-07 | Paper |
| Synthetic topology: of data types and classical spaces | 2013-08-27 | Paper |
Algorithmic solution of higher type equations
Journal of Logic and Computation | 2013-08-27 | Paper |
A constructive model of uniform continuity
Lecture Notes in Computer Science | 2013-06-28 | Paper |
Generalizations of Hedberg's theorem
Lecture Notes in Computer Science | 2013-06-28 | Paper |
| System T and the product of selection functions | 2012-09-18 | Paper |
The Peirce translation
Annals of Pure and Applied Logic | 2012-03-29 | Paper |
Sequential games and optimal strategies
Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences | 2011-12-17 | Paper |
Computational Interpretations of Analysis via Products of Selection Functions
Programs, Proofs, Processes | 2010-07-29 | Paper |
The Peirce translation and the double negation shift
Programs, Proofs, Processes | 2010-07-29 | Paper |
Computability of continuous solutions of higher-type equations
Mathematical Theory and Computational Practice | 2010-07-28 | Paper |
Selection functions, bar recursion and backward induction
Mathematical Structures in Computer Science | 2010-05-17 | Paper |
Operational domain theory and topology of sequential programming languages
Information and Computation | 2009-04-16 | Paper |
Exhaustible sets in higher-type computation
Logical Methods in Computer Science | 2008-11-13 | Paper |
Semantics of a sequential language for exact real-number computation
Theoretical Computer Science | 2007-07-16 | Paper |
Theory and Applications of Models of Computation
Lecture Notes in Computer Science | 2007-04-30 | Paper |
On the computational content of the Lawson topology
Theoretical Computer Science | 2006-08-16 | Paper |
Compactly generated Hausdorff locales
Annals of Pure and Applied Logic | 2005-12-06 | Paper |
On the non-sequential nature of the interval-domain model of real-number computation
Mathematical Structures in Computer Science | 2005-03-21 | Paper |
Comparing Cartesian closed categories of (core) compactly generated spaces
Topology and its Applications | 2004-10-01 | Paper |
| scientific article; zbMATH DE number 2103282 (Why is no real title available?) | 2004-09-24 | Paper |
Injective locales over perfect embeddings and algebras of the upper powerlocale monad
Applied General Topology | 2004-09-06 | Paper |
| scientific article; zbMATH DE number 2086646 (Why is no real title available?) | 2004-08-11 | Paper |
Joins in the frame of nuclei
Applied Categorical Structures | 2003-07-01 | Paper |
Integration in Real PCF
Information and Computation | 2003-01-14 | Paper |
| In Domain Realizability, not all Functionals on C[–1, 1] are Continuous | 2003-01-08 | Paper |
Function-space compactifications of function spaces
Topology and its Applications | 2002-08-22 | Paper |
The regular-locally compact coreflection of a stably locally compact locale
Journal of Pure and Applied Algebra | 2001-11-19 | Paper |
| scientific article; zbMATH DE number 1498617 (Why is no real title available?) | 2000-09-25 | Paper |
| scientific article; zbMATH DE number 1330442 (Why is no real title available?) | 1999-09-21 | Paper |
| scientific article; zbMATH DE number 1330441 (Why is no real title available?) | 1999-09-20 | Paper |
Properly injective spaces and function spaces
Topology and its Applications | 1999-09-06 | Paper |
The way-below relation of function spaces over semantic domains
Topology and its Applications | 1999-09-06 | Paper |
Induction and recursion on the partial real line with applications to Real PCF
Theoretical Computer Science | 1999-01-12 | Paper |
| scientific article; zbMATH DE number 1231643 (Why is no real title available?) | 1999-01-06 | Paper |
PCF extended with real numbers
Theoretical Computer Science | 1997-02-27 | Paper |
| scientific article; zbMATH DE number 860046 (Why is no real title available?) | 1996-07-16 | Paper |
| scientific article; zbMATH DE number 802425 (Why is no real title available?) | 1995-11-09 | Paper |
