Bas Spitters' articles
A version of this page with abstracts is available here. Some of my papers are on the Arxiv. My Google Scholar Profile. DBLP.
preprints

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

2013

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).

2012

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

2011
Computer certified efficient exact reals in Coq (with Robbert Krebbers)

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.

Metric complements of overt closed sets (jww Thierry Coquand and Erik Palmgren)

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

2010

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

2009
Intuitionistic quantum logic of an n-level system (with Martijn Caspers, Chris Heunen, Nicolaas P. Landsman)

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.

2007

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

2006

A constructive view on ergodic theorems
Journal of Symbolic Logic, June 2006, 71(2) pp. 611-623
pdf bib tm html

2005

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

2003

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