nLab Bas Spitters


Bas Spitters is professor for formal logic and computer science at Aarhus University and leader of the Concordium Blockchain Research Center


On constructive integration theory:

  • Bas Spitters, Constructive algebraic integration theory, Annals of Pure and Applied Logic, Volume 137, Issues 1–3, January 2006, Pages 380-390 (pdf, doi:10.1016/j.apal.2005.05.031)

  • Bas Spitters, Constructive algebraic integration theory without choice. In Thierry Coquand, Henri Lombardi, Marie-Francoise Roy, Mathematics, Algorithms, Proofs, 2005, Dagstuhl Seminar Proceedings 05021, Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany. (pdf)

On constructive analysis with exact real numbers via type theory:

and specifically with Type classes in Coq:


  • Bas Spitters, Verified Implementation of Exact Real Arithmetic in Type Theory, talk at Computable Analysis and Rigorous Numeric (2013) [pdf, pdf]

On Bohr toposes:

On mathematical structures formulated in dependent type theory, specifically via Type classes in Coq:

  • Bas Spitters, Eelis van der Wegen Type classes for mathematics in type theory, Mathematical Structures in Computer Science 21 4 “Interactive Theorem Proving and the Formalisation of Mathematics” (2011) 795-825 [doi:10.1017/S0960129511000119]

On software verification for blockchain-technology:

category: people

Last revised on September 3, 2023 at 20:26:46. See the history of this page for a list of all contributions to it.