| Publication | Date of Publication | Type |
|---|
| Type theory with explicit universe polymorphism | 2024-11-26 | Paper |
| Infinite objects in type theory | 2023-12-08 | Paper |
| Heitman dimension of distributive lattices and commutative rings | 2023-12-01 | Paper |
| A variation of Reynolds-Hurkens Paradox | 2023-08-31 | Paper |
| Reduction Free Normalisation for a proof irrelevant type of propositions | 2023-08-26 | Paper |
| Constructive Algebra and Point-Free Topology | 2023-08-11 | Paper |
| Constructive Theory of Ordinals | 2023-08-04 | Paper |
| Constructive Remarks on Azumaya Algebra | 2023-06-30 | Paper |
| A Foundation for Synthetic Algebraic Geometry | 2023-06-30 | Paper |
| Lorenzen's Proof of Consistency for Elementary Number Theory | 2023-06-14 | Paper |
| Some remarks about normal rings | 2022-10-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5089011 | 2022-07-18 | Paper |
| On generalized algebraic theories and categories with families | 2022-06-24 | Paper |
| Constructive sheaf models of type theory | 2022-06-24 | Paper |
| Formal Topology and Univalent Foundations | 2022-06-17 | Paper |
| Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism | 2022-04-07 | Paper |
| Canonicity and homotopy canonicity for cubical type theory | 2022-02-09 | Paper |
| Lorenzen and Constructive Mathematics | 2022-01-27 | Paper |
| Regular Entailment Relations | 2022-01-27 | Paper |
| Syntax and models of Cartesian cubical type theory | 2022-01-20 | Paper |
| A Sheaf Model of the Algebraic Closure | 2021-06-24 | Paper |
| Constructive basic theory of central simple algebras | 2021-02-25 | Paper |
| On Higher Inductive Types in Cubical Type Theory | 2021-01-20 | Paper |
| Inner Models of Univalence | 2021-01-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5144677 | 2021-01-19 | Paper |
| A Note on Generalized Algebraic Theories and Categories with Families | 2020-12-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3300787 | 2020-07-30 | Paper |
| Lorenzen's proof of consistency for elementary number theory [with an edition and translation of "Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis] | 2020-06-16 | Paper |
| Some Remarks about Normal Rings | 2020-04-03 | Paper |
| Skolem’s Theorem in Coherent Logic | 2020-01-24 | Paper |
| Regular entailment relations | 2019-12-19 | Paper |
| Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality | 2019-11-19 | Paper |
| Lattice-ordered groups generated by an ordered group and regular systems of ideals | 2019-10-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5195247 | 2019-09-18 | Paper |
| The univalence axiom in cubical sets | 2019-08-21 | Paper |
| An adequacy theorem for dependent type theory | 2019-07-04 | Paper |
| Canonicity and normalization for dependent type theory | 2019-06-18 | Paper |
| An application of constructive completeness | 2019-01-15 | Paper |
| R\'esolutions libres finies. M\'ethodes constructives | 2018-11-05 | Paper |
| Syntactic forcing models for coherent logic | 2018-10-08 | Paper |
| Combinatorial topology and constructive mathematics | 2018-10-08 | Paper |
| Cubical Type Theory: a constructive interpretation of the univalence axiom | 2018-08-13 | Paper |
| An elementary proof of Wiebe's theorem | 2018-03-01 | Paper |
| Hidden constructions in abstract algebra, Krull Dimension, Going Up, Going Down | 2017-12-13 | Paper |
| Constructions cach\'ees en alg\`ebre abstraite. Dimension de Krull, Going Up, Going Down (revised version, 2008) | 2017-12-13 | Paper |
| Constructive topology and combinatorics | 2017-11-17 | Paper |
| An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices (1951) | 2017-11-14 | Paper |
| The Independence of Markov's Principle in Type Theory. | 2017-10-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5367048 | 2017-10-12 | Paper |
| Type theory and formalisation of mathematics | 2017-08-22 | Paper |
| The Ackermann Award 2016 | 2017-07-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5277833 | 2017-07-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2980980 | 2017-05-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2968413 | 2017-03-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2967790 | 2017-03-02 | Paper |
| A presheaf model of parametric type theory | 2016-12-16 | Paper |
| A generalization of the Takeuti–Gandy interpretation | 2016-07-27 | Paper |
| Anneaux à diviseurs et anneaux de Krull (une approche constructive) | 2016-04-25 | Paper |
| Computing persistent homology within Coq/SSReflect | 2015-09-17 | Paper |
| A Computational Interpretation of Forcing in Type Theory | 2015-06-05 | Paper |
| Recursive Functions and Constructive Mathematics | 2015-05-19 | Paper |
| A Kripke model for simplicial sets | 2015-02-24 | Paper |
| Dynamic Newton–Puiseux theorem | 2014-11-20 | Paper |
| Isomorphism is equality | 2014-09-03 | Paper |
| Revisiting Zariski main theorem from a constructive point of view | 2014-08-28 | Paper |
| Constructive algebra | 2014-08-28 | Paper |
| A constructive version of Laplace's proof on the existence of complex roots | 2013-10-28 | Paper |
| Generalizations of Hedberg’s Theorem | 2013-06-28 | Paper |
| Coherent and Strongly Discrete Rings in Type Theory | 2013-04-19 | Paper |
| About Goodman's theorem | 2013-03-15 | Paper |
| Constructive theory of Banach algebras | 2012-12-17 | Paper |
| Unique paths as formal points | 2012-12-17 | Paper |
| A constructive proof of Simpson’s Rule | 2012-12-17 | Paper |
| The Ackermann Award 2012. | 2012-11-22 | Paper |
| Stop When You Are Almost-Full | 2012-09-20 | Paper |
| Constructive finite free resolutions | 2012-02-14 | Paper |
| A Decision Procedure for Regular Expression Equivalence in Type Theory | 2011-11-22 | Paper |
| Metric complements of overt closed sets | 2011-09-27 | Paper |
| Games with 1-backtracking | 2011-08-26 | Paper |
| A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance | 2011-05-26 | Paper |
| A Note on Forcing and Type Theory | 2011-01-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3062067 | 2011-01-03 | Paper |
| Curves and coherent Prüfer rings | 2010-11-19 | Paper |
| Spectral schemes as ringed lattices | 2010-03-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3400627 | 2010-02-05 | Paper |
| Constructive Gelfand duality for C*-algebras | 2009-10-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3395957 | 2009-09-15 | Paper |
| A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance | 2009-07-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3635860 | 2009-07-06 | Paper |
| CONSTRUCTIVE KRULL DIMENSION I: INTEGRAL EXTENSIONS | 2009-04-28 | Paper |
| Integrals and valuations | 2009-04-15 | Paper |
| Dimension de Heitmann des treillis distributifs et des anneaux commutatifs | 2009-04-14 | Paper |
| Space of valuations | 2009-03-25 | Paper |
| Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory | 2008-08-28 | Paper |
| Kolmogorov's contribution to intuitionistic logic | 2008-06-27 | Paper |
| A note on the axiomatisation of real numbers | 2008-06-12 | Paper |
| Automating Coherent Logic | 2008-05-27 | Paper |
| On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory | 2008-04-11 | Paper |
| Constructive Mathematics and Functional Programming (Abstract) | 2008-04-11 | Paper |
| A proof of strong normalisation using domain theory | 2008-04-01 | Paper |
| The projective spectrum as a distributive lattice | 2008-01-18 | Paper |
| Towards Constructive Homological Algebra in Type Theory | 2007-11-28 | Paper |
| Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems | 2007-10-15 | Paper |
| The completeness of typing for context-semantics | 2007-07-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3593498 | 2007-07-20 | Paper |
| A logical approach to abstract algebra | 2007-02-09 | Paper |
| On seminormality | 2006-12-07 | Paper |
| A Short Proof for the Krull Dimension of a Polynomial Ring | 2006-12-05 | Paper |
| Types for Proofs and Programs | 2006-11-13 | Paper |
| Frontiers of Combining Systems | 2006-10-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5483299 | 2006-08-16 | Paper |
| Remarks on the equational theory of non-normalizing pure type systems | 2006-03-22 | Paper |
| Geometric Hahn-Banach theorem | 2006-03-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5718574 | 2006-01-16 | Paper |
| New Computational Paradigms | 2006-01-11 | Paper |
| Typed Lambda Calculi and Applications | 2005-11-11 | Paper |
| Typed Lambda Calculi and Applications | 2005-11-11 | Paper |
| A nilregular element property | 2005-08-17 | Paper |
| A constructive proof of the Peter-Weyl theorem | 2005-08-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024822 | 2005-07-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4681364 | 2005-06-23 | Paper |
| A note on measures with values in a partially ordered vector space | 2005-06-13 | Paper |
| About Stone's notion of spectrum | 2005-04-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4665735 | 2005-04-11 | Paper |
| Generating non-Noetherian modules constructively | 2005-02-02 | Paper |
| Proof-theoretical analysis of order relations | 2004-12-16 | Paper |
| Remarks on the equational theory of non-normalizing pure type systems | 2004-09-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4813221 | 2004-08-13 | Paper |
| Hidden constructions in abstract algebra. Krull Dimension of distributive lattices and commutative rings | 2004-08-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4736389 | 2004-08-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4470492 | 2004-07-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4457452 | 2004-03-22 | Paper |
| On a theorem of Kronecker about algebraic varieties | 2004-03-15 | Paper |
| Inductively generated formal topologies. | 2003-11-25 | Paper |
| Metric Boolean algebras and constructive measure theory | 2003-09-16 | Paper |
| Compact spaces and distributive lattices. | 2003-09-15 | Paper |
| A syntactical proof of the Marriage Lemma. | 2003-01-21 | Paper |
| Valuations and Dedekind's Prague theorem | 2002-04-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2778814 | 2002-03-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4944848 | 2002-02-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2753679 | 2001-12-03 | Paper |
| Formal topologies on the set of first-order formulae | 2001-07-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4499170 | 2001-03-06 | Paper |
| Intuitionistic choice and classical logic | 2000-11-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4944905 | 2000-03-22 | Paper |
| A new method for establishing conservativity of classical systems over their intuitionistic version | 1999-11-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4247301 | 1999-10-05 | Paper |
| A Boolean model of ultrafilters | 1999-09-22 | Paper |
| On the computational content of the axiom of choice | 1999-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4218931 | 1999-04-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4225148 | 1999-01-18 | Paper |
| Two applications of Boolean models | 1998-08-10 | Paper |
| Intuitionistic model constructions and normalization proofs | 1998-03-23 | Paper |
| Minimal invariant spaces in formal topology | 1998-03-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4717191 | 1997-03-13 | Paper |
| A constructive topological proof of van der Waerden's theorem | 1996-07-16 | Paper |
| An algorithm for type-checking dependent types | 1996-07-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4855339 | 1996-04-16 | Paper |
| A semantics of evidence for classical arithmetic | 1996-01-21 | Paper |
| An analysis of Ramsey's theorem | 1995-11-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4325789 | 1995-09-18 | Paper |
| A-translation and looping combinators in pure type systems | 1995-06-11 | Paper |
| Another proof of the intuitionistic Ramsey theorem | 1994-12-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4282577 | 1994-09-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4289277 | 1994-05-24 | Paper |
| The paradox of trees in type theory | 1993-11-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4012882 | 1992-09-27 | Paper |
| An intuitionistic proof of Tychonoff's theorem | 1992-09-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4001132 | 1992-09-26 | Paper |
| Inheritance as implicit coercion | 1992-06-25 | Paper |
| The Wiener lemma and certain of its generalizations | 1992-06-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5753923 | 1990-01-01 | Paper |
| Categories of embeddings | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3204024 | 1989-01-01 | Paper |
| Domain theoretic models of polymorphism | 1989-01-01 | Paper |
| The calculus of constructions | 1988-01-01 | Paper |
| Extensional models for polymorphism | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3787462 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3775518 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3784072 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3030827 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3792655 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3703866 | 1985-01-01 | Paper |
| A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3708000 | 1984-01-01 | Paper |
| The Regular Element Property in Constructive Mathematics | N/A | Paper |
