| Publication | Date of Publication | Type |
|---|
| Design and implementation of the andromeda proof assistant | 2026-02-20 | Paper |
Comodule representations of second-order functionals
Journal of Logical and Algebraic Methods in Programming | 2025-08-08 | Paper |
| Incorporating a database of graphs into a proof assistant | 2024-12-04 | Paper |
| Analytica -- an experiment in combining theorem proving and symbolic computation | 2024-06-21 | Paper |
| MLFMF: Data Sets for Machine Learning for Mathematical Formalization | 2023-10-26 | Dataset |
Finitary type theories with and without contexts
Journal of Automated Reasoning | 2023-10-24 | Paper |
| Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem | 2023-07-15 | Paper |
Runners in Action
Programming Languages and Systems | 2022-10-13 | Paper |
Equality checking for general type theories in Andromeda 2
Lecture Notes in Computer Science | 2022-10-13 | Paper |
scientific article; zbMATH DE number 7577584 (Why is no real title available?)
(available as arXiv preprint) | 2022-08-30 | Paper |
| scientific article; zbMATH DE number 7577584 (Why is no real title available?) | 2022-08-30 | Paper |
An extensible equality checking algorithm for dependent type theories
(available as arXiv preprint) | 2022-02-09 | Paper |
| An extensible equality checking algorithm for dependent type theories | 2022-02-09 | Paper |
Instance reducibility and Weihrauch degrees
(available as arXiv preprint) | 2021-06-03 | Paper |
Five stages of accepting constructive mathematics
Bulletin of the American Mathematical Society | 2020-09-22 | Paper |
| A general definition of dependent type theories | 2020-09-11 | Paper |
Every metric space is separable in function realizability
(available as arXiv preprint) | 2019-05-24 | Paper |
On fixed-point theorems in synthetic computability
Tbilisi Mathematical Journal | 2017-12-08 | Paper |
| The HoTT Library: A formalization of homotopy type theory in Coq | 2016-10-14 | Paper |
An injection from the Baire space to natural numbers
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
On the failure of fixed-point theorems for chain-complete lattices in the effective topos
Electronic Notes in Theoretical Computer Science | 2016-05-10 | Paper |
An effect system for algebraic effects and handlers
Logical Methods in Computer Science | 2015-01-15 | Paper |
Programming with algebraic effects and handlers
Journal of Logical and Algebraic Methods in Programming | 2014-12-03 | Paper |
Cartesian closed categories of separable Scott domains
Theoretical Computer Science | 2014-07-25 | Paper |
A non-commutative Priestley duality.
Topology and its Applications | 2014-01-08 | Paper |
| First steps in synthetic computability theory | 2013-10-08 | Paper |
An effect system for algebraic effects and handlers
Algebra and Coalgebra in Computer Science | 2013-09-13 | Paper |
On the Bourbaki-Witt principle in toposes
Mathematical Proceedings of the Cambridge Philosophical Society | 2013-07-26 | Paper |
Stone Duality for Skew Boolean Algebras with Intersections
(available as arXiv preprint) | 2013-05-27 | Paper |
Implementing real numbers with RZ
Electronic Notes in Theoretical Computer Science | 2013-05-03 | Paper |
A relationship between equilogical spaces and type two effectivity
Electronic Notes in Theoretical Computer Science | 2013-04-26 | Paper |
On monadic parametricity of second-order functionals
Lecture Notes in Computer Science | 2013-03-18 | Paper |
Intuitionistic mathematics and realizability in the physical world
A Computable Universe | 2013-02-26 | Paper |
Similarity-based relations in Datalog programs
International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems | 2012-11-15 | Paper |
| Canonical effective subalgebras of classical algebras as constructive metric completions | 2012-09-28 | Paper |
On the failure of fixed-point theorems for chain-complete lattices in the effective topos
Theoretical Computer Science | 2012-05-30 | Paper |
Metric spaces in synthetic topology
Annals of Pure and Applied Logic | 2011-12-12 | Paper |
| Canonical effective subalgebras of classical algebras as constructive metric completions | 2011-02-10 | Paper |
| Similarity measures for relational databases | 2009-07-22 | Paper |
A constructive theory of continuous domains suitable for implementation
Annals of Pure and Applied Logic | 2009-06-11 | Paper |
RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
Journal Of Logic And Computation | 2009-03-02 | Paper |
Sheaf toposes for realizability
Archive for Mathematical Logic | 2008-08-18 | Paper |
RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
Lecture Notes in Computer Science | 2007-11-13 | Paper |
Two constructive embedding‐extension theorems with applications to continuity principles and to Banach‐Mazur computability
Mathematical Logic Quarterly | 2005-02-16 | Paper |
Propositions as [Types]
Journal Of Logic And Computation | 2004-10-28 | Paper |
| scientific article; zbMATH DE number 2086646 (Why is no real title available?) | 2004-08-11 | Paper |
Equilogical spaces
Theoretical Computer Science | 2004-08-06 | Paper |
| A Relationship between Equilogical Spaces and Type Two Effectivity | 2003-11-30 | Paper |
| scientific article; zbMATH DE number 1670478 (Why is no real title available?) | 2001-12-03 | Paper |
| scientific article; zbMATH DE number 1531356 (Why is no real title available?) | 2001-02-28 | Paper |
Multibasic and mixed hypergeometric Gosper-type algorithms
Journal of Symbolic Computation | 2000-05-08 | Paper |
Analytica --- an experiment in combining theorem proving and symbolic computation
Journal of Automated Reasoning | 1999-06-29 | Paper |
The Countable Reals
(available as arXiv preprint) | N/A | Paper |
