nLab Bas Spitters

 Selected writings

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

 Selected writings

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:

Exposition:

  • 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 modalities in homotopy type theory (modal homotopy type theory):

On software verification for blockchain-technology:

category: people

Last revised on February 15, 2024 at 15:10:46. See the history of this page for a list of all contributions to it.