Bas Spitters, Steven Vickers, and Sander Wolters ** Gelfand spectra in Grothendieck toposes using geometric mathematics**,
1310.0705, 2013.
revision for QPL 2012 post-proceedings in EPTCS.

Egbert Rijke, Bas Spitters **Sets in homotopy type theory**

ArXiV 1305.3835, 2013.
under revision for the special issue of MSCS on homotopy type theory bib

Orthogonal factorization systems in homotopy type theory (Egbert Rijke and Bas Spitters), 2013.

PDF

The Univalent Foundations Program, ** Homotopy Type Theory: Univalent Foundations of Mathematics**, Institute for Advanced Study, Web page, 1308.0729, 2013. bib Coq code

**Press:** Communications of the ACM, Wired, Images de Maths,
ACM notable book.

Evgeny Makarov and Bas Spitters **The Picard Algorithm for Ordinary Differential Equations in Coq**
Rough Diamond in ITP2013, pdf (sources), (bib), 2013.

**Type classes for efficient exact real arithmetic in Coq** (with Robbert Krebbers)

LMCS 9(1:1), 2013. 10.2168/LMCS-9(1:01)2013. PDF 1106.3448. sources (bib).

Proceedings 8th International Workshop on Quantum Physics and Logic (jww Bart Jacobs,
Peter Selinger)

EPTCS 95, arXiv:1210.0298, 10.4204/EPTCS.95, 2012
ISSN: 2075-2180

**A constructive proof of Simpson's Rule** (jww Thierry Coquand)

Logic and Analysis 4:15 (2012) 1-8. 1202.3460 PDF bib.

**The Space of Measurement Outcomes as a Spectral Invariant for Non-Commutative Algebras**

Foundations of Physics 10.1007/s10701-011-9619-3, 2012.
bib

**Bohrification of operator algebras and quantum logic** (with Chris Heunen
and Klaas Landsman)

Synthese, 1-34, 2012, 10.1007/s11229-011-9918-4. ArXiv:0905.2275. bib

1105.2751. CICM'11 LNCS 90-106, 2011. 10.1007/978-3-642-22673-1_7. PDF, bib, sources.

**The Gelfand spectrum of a noncommutative C*-algebra: a topos-theoretic approach** (with Chris Heunen and Klaas Landsman and Sander Wolters)

J. Australian Math. Soc. 10.1017/S1446788711001157, PDF bib

**Bohrification** (with Chris Heunen and Klaas Landsman)

Available in the arxiv as 0909.3468. bib

In Deep Beauty (ed Hans Halvorson), Cambridge University Press, 2011.

Mathematical Logic Quarterly, 57(4), 373-378, 2011. 10.1002/malq.201010011 ArXiv:0906.3433. bib

**Type Classes for Mathematics in Type Theory** (with Eelis van der Weegen).

*Interactive theorem proving and the formalization of mathematics*, Special Issue of Mathematical Structures in Computer Science, 21, 1-31, 2011 10.1017/S0960129511000119.
(A shorter version `Developing the algebraic hierarchy with type classes in Coq' appeared as a *Rough Diamond* at ITP-10).
ArXiv 1102.1323.
development.
bib

**The space of measurement outcomes as a spectrum for a non-commutative algebras**

1006.1432 Published in EPTCS special issue for DCM.
bib

**A Constructive Theory of Banach algebras** (jww Thierry Coquand)

Logic and Analysis, 2:11 (2010) 1-15. PDF. Preprint available in the arxiv as 1002.4011bib.

**Locatedness and overt sublocales**

doi:10.1016/j.apal.2010.07.002 APAL. Available in the arxiv
as 0703561.
bib

**A computer verified, monadic, functional implementation of the integral.** (with Russell O'Connor)

Theoretical Computer Science. Volume 411, Issue 37, 7 August 2010, Pages 3386-3402 doi:10.1016/j.tcs.2010.05.031. Available at the arxiv as 0809.1552 bib

**Constructive pointfree topology eliminates non-constructive
representation theorems from Riesz space theory.**

DOI 10.1007/s11083-010-9147-3
Order 27(2), Springer 2010.

Paper.
Arxiv: 0807.2454 bib

Foundations of Physics 39(7):731-759, 2009. Available at the arxiv as 0902.3201 bib

**A topos for algebraic quantum theory** (with Chris Heunen and Klaas Landsman)

Communications mathematical physics 291(1) 63-110. Available at the arxiv as 0709.4364. bib

Integrals and Valuations (with Thierry Coquand)

Logic and Analysis 1(3) p1-22. Available at the arxiv as 0808.1522 bib

**Constructive Gelfand duality for C*-algebras** (with Thierry Coquand)

Mathematical Proceedings of the Cambridge Philosophical society Volume 147, Issue 02, September 2009, pp 323-337. doi:10.1017/S0305004109002539 Available at the arxiv as 0808.1518 bib.

**The principle of general tovariance** (with Chris Heunen and Klaas Landsman) Proc.
XVI International Fall Workshop on Geometry and Physics (Lisbon, 2007), editor R. Picken et al., American Physical Society, 2008.

00003931
bib

**Constructive analysis, types and exact real numbers.**
(with
Herman Geuvers,
Milad Niqui
and
Freek Wiedijk)

Constructive analysis, types and exact real numbers, special
issue of Mathematical Structures in Computer Science (Bas
Spitters, Herman Geuvers, Milad Niqui and Freek Wiedijk(eds.))
MSCS
Volume 17, Issue 01, pp 3-36, 2007.

doi:10.1017/S0960129506005834
pdf
bib

**A constructive view on ergodic theorems**

Journal of Symbolic Logic, June 2006, 71(2) pp. 611-623

pdf
bib
tm
html

**Constructive Results on Operator Algebras**

Journal of
Universal computation volume 11, issue 12
2005.

ps.gz
pdf
bib
tm
html

**Formal Topology and Constructive Mathematics: the
Gelfand and Stone-Yosida Representation Theorems** (with Thierry Coquand)

Journal of
Universal computation volume 11, issue 12
2005.

A slightly expanded version is available here.
bib
tm
html

**Constructive algebraic integration theory without choice**

In: Thierry Coquand and Henri Lombardi and Marie-Francoise Roy,
Mathematics, Algorithms, Proofs, Dagstuhl Seminar Proceedings 05021,
Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss
Dagstuhl, Germany.

pdf
bib

**Almost periodic functions, constructively**

LMCS
Volume 1, issue 3, paper 4, 2005.

The paper can be downloaded here.
bib

**A constructive proof of the Peter-Weyl theorem**
(with Thierry
Coquand)

Mathematical Logic Quarterly. Vol. 4, 2005, page 351-359. Wiley VCH

pdf
bib

**Approximating integrable sets by compacts
constructively.**

in
From Sets and Types to Topology and Analysis - Towards
Practicable Foundations for Constructive Mathematics, Laura Crosilla
and Peter Schuster (eds.)

ps
ps.gz
pdf
bib

**Constructive Algebraic Integration theory.**

*Annals
of Pure and Applied Logic*. Elsevier, 2005

doi:10.1016/j.apal.2005.05.031

ps
ps.gz
pdf
bib

**Program
extraction from large proof developments.** (with Lu�s Cruz-Filipe).

in *Proceedings of 16th International Conference TPHOLs 2003
(in LNCS
proceedings),* D. Basin and B. Wolff (eds.), pages
205--220, LNCS 2758, 2003 Springer-Verlag 2003
ps,
ps.gz,
pdf,
bib.

**Locating the range of an operator with an adjoint.**
(with Douglas
Bridges and Hajime Ishihara)

*Indagationes Mathematicae,* 13(4):433-440, 2003. �
Elsevier, 2002

ps
ps.gz
pdf
bib

**Located Operators.**

*Mathematical Logic Quarterly,* 48(Suppl. 1):107-122,
2002. Wiley, VCH 2002

pdf
bib

**Constructive and intuitionistic integration theory
and functional analysis.**

Ph. D. thesis, University of Nijmegen, 2002

pdf
bib

**A constructive converse of the mean value theorem.**
(with Wim
Veldman)

*Indagationes Mathematicae,* 11(1):151-157, 2000.
Elsevier, 2000

ps
ps.gz
pdf
bib

Publishers self-archiving rules, DOI look up, OA DOI resolver

To my homepage