# Bas Spitters

This page needs updating.

#### Research interests

- Constructive mathematics: type theory and topos theory
- Computer mathematics, interactive theorem proving
- Logical and categorical foundations of physics

2015: Associate professor at CMU working on the MURI grant Homotopy Type Theory: Unified Foundations of Mathematics and Computation

and Aarhus in the Logic and Semantics Group.

2014: Visiting positions at LRI Paris-Sud, IHP, PPS Paris-7, Gotheburg Computing Science.

2013: Member of the Institute for Advanced Studies for the special year on univalent foundations.

2010-2013: Leading the Nijmegen contribution to the ForMath project, as well as Work Package 4: formalization of exact analysis. (The project got an "excellent" mark.)

Publications
Talks

Videos

PCs:

- Mathematics: Algorithms and Proofs (MAP07(report), MAP11(report))
- Computability and Complexity in Analysis (CCA08)
- Mathematical Logic in the Netherlands (MLNL09, MLNL10)
- Coq workshop (Coq-2, Coq-3, Coq-4, Coq-7 (2015))
- Workshop on Logic, Language, Information and Computation (WoLLIC11)
- Interactive Theorem Proving (ITP2012, ITP2014))
- Quantum Physics and Logic (QPL-11, QPL-12, QPL-13, QPL-14, QPL-15)
- Higher Dimensional Algebra, Categories and Types (HDACT)
- Certified Programs and Proofs (CPP13)
- Calculemus 15
- TYPES2015

Organization: PhDay'01, Constructive mathematics, types and exact real numbers, DIAMANT-day '05,
Brouwer seminar (from 2004 to 2007), MAP07,
Sheaves in Geometry and Quantum Theory, MLNL09, QPL-11, Coq-workshop 2011, MAP11, Type Theory And Formalization Of Mathematics

Homotopy Type Theory and Univalent Foundations - Mini-Symposium at DMV 2015.

CIRM workshop: Computable Analysis: Foundations, Implementation and Certification.

The constructivenews-list.

DIAMANT researcher.

Previous grants: VENI `Reasoning and Computing' of the dutch science foundation NWO.
##### PhD-students

Egbert Rijke (2012-2013).

Eelis van der Weegen (2010-2011).

Russell O'Connor Incompleteness and Completeness Formalizing Logic and Analysis in Type Theory (2005-2008).

Onderwijs Seminar on simplicial methods (2012)

PGP