| Publication | Date of Publication | Type |
|---|
| 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 | 2023-10-24 | Paper |
| Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem | 2023-07-15 | Paper |
| Runners in Action | 2022-10-13 | Paper |
| Equality Checking for General Type Theories in Andromeda 2 | 2022-10-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5101353 | 2022-08-30 | Paper |
| An extensible equality checking algorithm for dependent type theories | 2022-02-09 | Paper |
| Instance reducibility and Weihrauch degrees | 2021-06-03 | Paper |
| Five stages of accepting constructive mathematics | 2020-09-22 | Paper |
| A general definition of dependent type theories | 2020-09-11 | Paper |
| Every metric space is separable in function realizability | 2019-05-24 | Paper |
| On fixed-point theorems in synthetic computability | 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 | 2016-07-27 | Paper |
| On the failure of fixed-point theorems for chain-complete lattices in the effective topos | 2016-05-10 | Paper |
| An Effect System for Algebraic Effects and Handlers | 2015-01-15 | Paper |
| Programming with algebraic effects and handlers | 2014-12-03 | Paper |
| Cartesian closed categories of separable Scott domains | 2014-07-25 | Paper |
| A non-commutative Priestley duality. | 2014-01-08 | Paper |
| First steps in synthetic computability theory | 2013-10-08 | Paper |
| An Effect System for Algebraic Effects and Handlers | 2013-09-13 | Paper |
| On the Bourbaki-Witt principle in toposes | 2013-07-26 | Paper |
| Stone Duality for Skew Boolean Algebras with Intersections | 2013-05-27 | Paper |
| Implementing Real Numbers With RZ | 2013-05-03 | Paper |
| A Relationship between Equilogical Spaces and Type Two Effectivity | 2013-04-26 | Paper |
| On Monadic Parametricity of Second-Order Functionals | 2013-03-18 | Paper |
| Intuitionistic Mathematics and Realizability in the Physical World | 2013-02-26 | Paper |
| SIMILARITY-BASED RELATIONS IN DATALOG PROGRAMS | 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 | 2012-05-30 | Paper |
| Metric spaces in synthetic topology | 2011-12-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3075211 | 2011-02-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5320785 | 2009-07-22 | Paper |
| A constructive theory of continuous domains suitable for implementation | 2009-06-11 | Paper |
| RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice | 2009-03-02 | Paper |
| Sheaf toposes for realizability | 2008-08-18 | Paper |
| RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice | 2007-11-13 | Paper |
| Two constructive embedding‐extension theorems with applications to continuity principles and to Banach‐Mazur computability | 2005-02-16 | Paper |
| Propositions as [Types] | 2004-10-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4737182 | 2004-08-11 | Paper |
| Equilogical spaces | 2004-08-06 | Paper |
| A Relationship between Equilogical Spaces and Type Two Effectivity | 2003-11-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2753674 | 2001-12-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4513573 | 2001-02-28 | Paper |
| Multibasic and mixed hypergeometric Gosper-type algorithms | 2000-05-08 | Paper |
| Analytica --- an experiment in combining theorem proving and symbolic computation | 1999-06-29 | Paper |
| The Countable Reals | N/A | Paper |
