# Bas Spitters

picture.

Associate professor in
the Logic and
Semantics Group, Dept. of Comp. Science, Aarhus University.

Office: Turing 229
Aabogade 34 DK-8200 Aarhus N, Denmark.
e-mail

In fall 2015 I am teaching a PhD-course on Homotopy type theory: Univalent Foundations of Mathematics.

#### Research interests

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

Publications
Talks

Videos

#### CV

Since April 2015: Aarhus University

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

PCs:

- Mathematics: Algorithms and Proofs (MAP07(report), MAP11(report)) MAP14
- 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, CPP18)
- Calculemus 15)
- TYPES2015
- Formal Structures for Computation and Deduction (FSCD17)

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.

**Grant**
Villum Foundation: Guarded Homotopy Type Theory. With Lars Birkedal we received 3.3 Mkr from the Villum Foundation for a research project on Guarded Homotopy Type Theory. The goal of the project is to develop new theories for and prototypes of proof assistants, which can be used within both mathematics and computer science.

Previous grants:

DIAMANT researcher.

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

Education Seminar on simplicial methods (2012)

PGP