Bas Spitters' articles
Some of my papers are on the Arxiv and e-print. My Google Scholar Profile DBLP Semantic Scholar zbmath ORCID .
preprints

Bas Spitters, Cubical sets and the topological topos 1610.05270

2020

Søren Eller Thomsen, Bas Spitters, Formalizing Nakamoto-Style Proof of Stake2007.12105, 2020
Emil Holm Gjørup, Bas Spitters, Congruence closure in cubical type theory PDF, 2020
Egbert Rijke, Michael Shulman, Bas Spitters, Modalities in homotopy type theory 1706.07526, LMCS, 16 (1), 2020
Daniel Huang, Greg Morrisett, Bas Spitters, An Application of Computable Distributions to the Semantics of Probabilistic Programs1806.07966 in Foundations of Probabilistic Programming link, 2020

2019

Martin E. Bidlingmaier, Florian Faissole, Bas Spitters, Synthetic topology in Homotopy Type Theory for probabilistic programming ArXiv
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters, ConCert: A Smart Contract Certification Framework in Coq ArXiv in CPP'20
Earlier version: Danil Annenkov and Bas Spitters, Towards a Smart Contract Verification Framework in Coq (in TYPES'19)
Jakob Botsch Nielsen and Bas Spitters, Smart Contract Interactions in Coq, ArXiv in FMBC'19

2018
Jonathan Sterling, Bas Spitters, Normalization by gluing for free λ-theories1809.08646
Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters, Modal Dependent Type Theory and Dependent Right Adjoints 1804.05236 Mathematical Structures in Computer Science, 1-21, 2019, DOI (2pp abstract at TYPES18)
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub, Computer-aided proofs for multiparty computation with active security PDF (CSF18) (e-print 502) code
Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters, Internal Universes in Models of Homotopy Type Theory1801.07664 FSCD18DOI

Florian Faissole and Bas Spitters, Synthetic topology in Homotopy Type Theory for probabilistic programming PDF Extended abstract accepted for PPS17 and CoqPL17

Preuves constructives de programmes probabilistes in JFLA PDF at HAL
2016

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, The HoTT Library: A formalization of homotopy type theory in Coq 1610.04591 (CPP17) pp. 164-172, 2017 10.1145/3018610.3018615 bib

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi, Guarded cubical type theory 1611.09263 bib (2016). journal version of:

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi, Guarded cubical type theory: Path Equality for Guarded Recursion CSL2016 1606.05223 (2016).

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi, Guarded cubical type theory abstract TYPES (2016) PDF

Expository paper: Egbert Rijke and Bas Spitters, Homotopy type theory and the formalization of mathematics, pp 159-164 (2016) in Special issue of Nieuw Archief voor Wiskunde on Wiskunde en computers (English: Mathematics and computers), Jan Bouwe van den Berg, Bas Spitters, Frank Vallentin (eds).PDF

2015

Bas Spitters, Cubical sets as a classifying topos TYPES (2015) PDF

2014

Egbert Rijke, Bas Spitters Sets in homotopy type theory
ArXiV 1305.3835, special issue "From type theory and homotopy theory to univalent foundations" of MSCS bibPDF

Bas Spitters, Steven Vickers, and Sander Wolters Gelfand spectra in Grothendieck toposes using geometric mathematics, EPTCS 158, 2014, pp. 77-107, 1310.0705 in the QPL2012 post-proceedings bib.

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 (or rchive.it), DOI look up, OA DOI resolver

To my homepage