| Publication | Date of Publication | Type |
|---|
Synthetic topology in Homotopy Type Theory for probabilistic programming
Mathematical Structures in Computer Science | 2022-12-09 | Paper |
Extracting functional programs from Coq, in Coq
Journal of Functional Programming | 2022-09-02 | Paper |
| Gelfand spectra in Grothendieck toposes using geometric mathematics | 2021-06-23 | Paper |
Gelfand spectra in Grothendieck toposes using geometric mathematics
(available as arXiv preprint) | 2021-06-23 | Paper |
Internal universes in models of homotopy type theory
(available as arXiv preprint) | 2021-06-15 | Paper |
| The space of measurement outcomes as a spectrum for non-commutative algebras | 2021-02-16 | Paper |
Modal dependent type theory and dependent right adjoints
Mathematical Structures in Computer Science | 2020-03-11 | Paper |
Modalities in homotopy type theory
(available as arXiv preprint) | 2020-01-22 | Paper |
Guarded cubical type theory
Journal of Automated Reasoning | 2019-08-21 | Paper |
Guarded cubical type theory
Journal of Automated Reasoning | 2019-08-21 | Paper |
Guarded cubical type theory: path equality for guarded recursion
(available as arXiv preprint) | 2017-07-19 | Paper |
| Homotopy type theory and the formalization of mathematics | 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
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
Bohrification of operator algebras and quantum logic
Synthese | 2013-11-25 | Paper |
The Picard Algorithm for Ordinary Differential Equations in Coq
Interactive Theorem Proving | 2013-08-07 | Paper |
Type classes for efficient exact real arithmetic in \textsc{Coq}
(available as arXiv preprint) | 2013-04-09 | Paper |
The space of measurement outcomes as a spectral invariant for non-commutative algebras
Foundations of Physics | 2013-01-07 | Paper |
Constructive theory of Banach algebras
Journal of Logic and Analysis | 2012-12-17 | Paper |
A constructive proof of Simpson's rule
Journal of Logic and Analysis | 2012-12-17 | Paper |
scientific article; zbMATH DE number 5977109 (Why is no real title available?)
(available as arXiv preprint) | 2011-11-22 | Paper |
Type classes for mathematics in type theory
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
Metric complements of overt closed sets
Mathematical Logic Quarterly | 2011-09-27 | Paper |
Locatedness and overt sublocales
Annals of Pure and Applied Logic | 2011-09-12 | Paper |
Computer Certified Efficient Exact Reals in Coq
Lecture Notes in Computer Science | 2011-07-29 | Paper |
The Gelfand spectrum of a noncommutative \(C^*\)-algebra: a topos-theoretic approach
Journal of the Australian Mathematical Society | 2011-06-29 | Paper |
Developing the algebraic hierarchy with type classes in Coq
Interactive Theorem Proving | 2010-09-14 | Paper |
A computer-verified monadic functional implementation of the integral
Theoretical Computer Science | 2010-08-24 | Paper |
Constructive pointfree topology eliminates non-constructive representation theorems from Riesz space theory
Order | 2010-07-02 | Paper |
Program extraction from large proof developments
Lecture Notes in Computer Science | 2010-05-07 | Paper |
A topos for algebraic quantum theory
Communications in Mathematical Physics | 2010-01-11 | Paper |
Intuitionistic quantum logic of an \(n\)-level system
Foundations of Physics | 2009-10-21 | Paper |
Constructive Gelfand duality for C*-algebras
Mathematical Proceedings of the Cambridge Philosophical Society | 2009-10-19 | Paper |
Integrals and valuations
Journal of Logic and Analysis | 2009-04-15 | Paper |
| The principle of general tovariance | 2008-11-17 | Paper |
| Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems | 2007-10-15 | Paper |
Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems
(available as arXiv preprint) | 2007-10-15 | Paper |
| Constructive results on operator algebras | 2007-10-15 | Paper |
Almost periodic functions, constructively
Logical Methods in Computer Science | 2007-10-11 | Paper |
Constructive analysis, types and exact real numbers
Mathematical Structures in Computer Science | 2007-04-12 | Paper |
Corrigendum to: ‘A constructive view on ergodic theorems’
Journal of Symbolic Logic | 2007-01-19 | Paper |
A constructive view on ergodic theorems
Journal of Symbolic Logic | 2006-08-03 | Paper |
| scientific article; zbMATH DE number 2247264 (Why is no real title available?) | 2006-01-16 | Paper |
Constructive algebraic integration theory
Annals of Pure and Applied Logic | 2005-12-06 | Paper |
A constructive proof of the Peter-Weyl theorem
MLQ | 2005-08-01 | Paper |
Locating the range of an operator with an adjoint
Indagationes Mathematicae. New Series | 2003-08-07 | Paper |
| Located Operators | 2002-01-01 | Paper |
A constructive converse of the mean value theorem
Indagationes Mathematicae. New Series | 2001-06-28 | Paper |
