| Publication | Date of Publication | Type |
|---|
| Synthetic topology in Homotopy Type Theory for probabilistic programming | 2022-12-09 | Paper |
| Extracting functional programs from Coq, in Coq | 2022-09-02 | Paper |
| Gelfand spectra in Grothendieck toposes using geometric mathematics | 2021-06-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4993352 | 2021-06-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5151024 | 2021-02-16 | Paper |
| Modal dependent type theory and dependent right adjoints | 2020-03-11 | Paper |
| Modalities in homotopy type theory | 2020-01-22 | Paper |
| Guarded cubical type theory | 2019-08-21 | Paper |
| Guarded Cubical Type Theory: Path Equality for Guarded Recursion | 2017-07-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2988057 | 2017-05-18 | Paper |
| Cubical sets and the topological topos | 2016-10-17 | Paper |
| The HoTT Library: A formalization of homotopy type theory in Coq | 2016-10-14 | Paper |
| Sets in homotopy type theory | 2016-07-27 | Paper |
| Bohrification of operator algebras and quantum logic | 2013-11-25 | Paper |
| The Picard Algorithm for Ordinary Differential Equations in Coq | 2013-08-07 | Paper |
| Type classes for efficient exact real arithmetic in Coq | 2013-04-09 | Paper |
| The space of measurement outcomes as a spectral invariant for non-commutative algebras | 2013-01-07 | Paper |
| Constructive theory of Banach algebras | 2012-12-17 | Paper |
| A constructive proof of Simpson’s Rule | 2012-12-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3100022 | 2011-11-22 | Paper |
| Type classes for mathematics in type theory | 2011-10-21 | Paper |
| Metric complements of overt closed sets | 2011-09-27 | Paper |
| Locatedness and overt sublocales | 2011-09-12 | Paper |
| Computer Certified Efficient Exact Reals in Coq | 2011-07-29 | Paper |
| THE GELFAND SPECTRUM OF A NONCOMMUTATIVE C*-ALGEBRA: A TOPOS-THEORETIC APPROACH | 2011-06-29 | Paper |
| Developing the Algebraic Hierarchy with Type Classes in Coq | 2010-09-14 | Paper |
| A computer-verified monadic functional implementation of the integral | 2010-08-24 | Paper |
| Constructive pointfree topology eliminates non-constructive representation theorems from Riesz space theory | 2010-07-02 | Paper |
| Program Extraction from Large Proof Developments | 2010-05-07 | Paper |
| A topos for algebraic quantum theory | 2010-01-11 | Paper |
| Intuitionistic quantum logic of an \(n\)-level system | 2009-10-21 | Paper |
| Constructive Gelfand duality for C*-algebras | 2009-10-19 | Paper |
| Integrals and valuations | 2009-04-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3535984 | 2008-11-17 | Paper |
| Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems | 2007-10-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5310892 | 2007-10-15 | Paper |
| Almost periodic functions, constructively | 2007-10-11 | Paper |
| Constructive analysis, types and exact real numbers | 2007-04-12 | Paper |
| Corrigendum to: ‘A constructive view on ergodic theorems’ | 2007-01-19 | Paper |
| A constructive view on ergodic theorems | 2006-08-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5718576 | 2006-01-16 | Paper |
| Constructive algebraic integration theory | 2005-12-06 | Paper |
| A constructive proof of the Peter-Weyl theorem | 2005-08-01 | Paper |
| Locating the range of an operator with an adjoint | 2003-08-07 | Paper |
| Located Operators | 2002-01-01 | Paper |
| A constructive converse of the mean value theorem | 2001-06-28 | Paper |
