| Publication | Date of Publication | Type |
|---|
| https://portal.mardi4nfdi.de/entity/Q6060678 | 2023-11-03 | Paper |
| From type theory to setoids and back | 2023-04-19 | Paper |
| EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS | 2021-01-29 | Paper |
| Categories with families and first-order logic with dependent sorts | 2019-10-07 | Paper |
| A CONSTRUCTIVE EXAMINATION OF A RUSSELL-STYLE RAMIFIED TYPE THEORY | 2018-05-03 | Paper |
| A Constructive Examination of a Russell-style Ramified Type Theory | 2017-04-22 | Paper |
| A constructive examination of rectifiability | 2017-04-10 | Paper |
| Constructions of categories of setoids from proof-irrelevant families | 2017-02-24 | Paper |
| Constructivist Versus Structuralist Foundations | 2015-06-05 | Paper |
| Constructing categories and setoids of setoids in type theory | 2014-09-30 | Paper |
| Formal continuity implies uniform continuity near compact images on metric spaces | 2014-03-21 | Paper |
| A generalized cut characterization of the fullness axiom in CZF | 2013-06-11 | Paper |
| Yet another category of setoids with equality on objects | 2013-04-21 | Paper |
| Open sublocales of localic completions | 2012-12-17 | Paper |
| A note on Brouwer’s weak continuity principle and the transfer principle in nonstandard analysis | 2012-12-17 | Paper |
| Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets | 2012-09-06 | Paper |
| Double sequences, almost Cauchyness and BD-N | 2012-08-01 | Paper |
| A predicative completion of a uniform space | 2012-06-01 | Paper |
| Proof-relevance of families of setoids and identity in type theory | 2012-02-10 | Paper |
| Metric complements of overt closed sets | 2011-09-27 | Paper |
| Introduction: The Three Foundational Programmes | 2009-03-12 | Paper |
| From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory | 2009-03-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3522669 | 2008-09-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5454624 | 2008-03-31 | Paper |
| Resolution of the uniform lower bound problem in constructive analysis | 2008-03-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5310884 | 2007-10-15 | Paper |
| Internalising modified realisability in constructive type theory | 2007-10-11 | Paper |
| A constructive and functorial embedding of locally compact metric spaces into locales | 2007-05-30 | Paper |
| Partial Horn logic and Cartesian categories | 2007-02-14 | Paper |
| Binary refinement implies discrete exponentiation | 2007-01-29 | Paper |
| Quotient topologies in constructive set theory and type theory | 2006-08-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5480940 | 2006-08-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5477360 | 2006-07-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5718569 | 2006-01-16 | Paper |
| Maximal and partial points in formal spaces | 2005-12-06 | Paper |
| Regular universes and formal spaces | 2005-12-06 | Paper |
| Constructive completions of ordered sets, groups and fields | 2005-08-25 | Paper |
| A categorical version of the BrouwerHeytingKolmogorov interpretation | 2004-05-27 | Paper |
| Metric Boolean algebras and constructive measure theory | 2003-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4552745 | 2003-05-12 | Paper |
| Wellfounded trees in categories | 2003-05-08 | Paper |
| Type theories, toposes and constructive set theory: Predicative aspects of AST | 2002-12-03 | Paper |
| An Intuitionistic Axiomatisation of Real Closed Fields | 2002-05-29 | Paper |
| Real numbers in the topos of sheaves over the category of filters | 2001-12-21 | Paper |
| Constructive nonstandard representations of generalized functions | 2001-06-28 | Paper |
| Intuitionistic choice and classical logic | 2000-11-05 | Paper |
| An Effective Conservation Result for Nonstandard Arithmetic | 2000-07-27 | Paper |
| Hyperfinite type structures | 2000-06-22 | Paper |
| Constructive Sheaf Semantics | 2000-04-06 | Paper |
| Inaccessibility in constructive set theory and type theory | 1999-11-23 | Paper |
| Developments in Constructive Nonstandard Analysis | 1999-08-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4247308 | 1999-06-16 | Paper |
| Minimal models of Heyting arithmetic | 1998-11-02 | Paper |
| A logical presentation of the continuous functionals | 1998-02-02 | Paper |
| A sheaf-theoretic foundation for nonstandard analysis | 1998-01-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4893100 | 1996-09-01 | Paper |
| The Friedman‐Translation for Martin‐Löf's Type Theory | 1995-12-13 | Paper |
| A constructive approach to nonstandard analysis | 1995-07-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4312460 | 1994-11-08 | Paper |
| A note on Mathematics of infinity | 1994-09-01 | Paper |
| An information system interpretation of Martin-Löf's partial type theory with universes | 1994-06-14 | Paper |
| Type-theoretic interpretation of iterated, strictly positive inductive definitions | 1994-05-23 | Paper |
| Remarks on Martin-Löf's partial type theory | 1993-11-28 | Paper |
| A construction of type: type in Martin-Löf's partial type theory with one universe | 1992-06-27 | Paper |
| Domain interpretations of Martin-Löf's partial type theory | 1990-01-01 | Paper |
