Bas Spitters
picture.
Associate professor in
the Logic and
Semantics Group, Dept. of Computer Science, Aarhus University.
Office: Turing-119
Aabogade 34 DK-8200 Aarhus N, Denmark.
e-mail
Research interests
I am leading the Concordium
Blockchain Research Center and the Blockchain workpackage in Digit.
Part of the Aarhus Quantum campus
Publications
Talks
Videos
CV
Since April 2015: Associate professor, 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
- ITP'23
- ACT'23
- POPL22
- IEEE International Conference on Blockchain and Cryptocurrency 2021
- Formal Methods for Blockchains (2019,2020,2024)
- CICM19
- CIRM workshop: Computable Analysis: Foundations, Implementation and Certification
- Homotopy Type Theory and Univalent Foundations - Mini-Symposium at DMV 2015
- Sheaves in Geometry and Quantum Theory, MLNL09, QPL-11, Coq-workshop 2011, MAP11, Type Theory And Formalization Of Mathematics
- Mathematics: Algorithms and Proofs
(MAP07(report), MAP11(report)) MAP14, MAP16
- Certified Programs and Proofs (CPP13,
CPP18,
CPP22,
CPP24
)
- Calculemus 15
- TYPES2015, TYPES'24
- Formal Structures for Computation and Deduction
(FSCD17)
- Coq workshop
(Coq-2, Coq-3, Coq-4, Coq-7
(2015)), 2018
- Interactive Theorem Proving (ITP2012, ITP2014,
ITP2022,
ITP2023)
- Workshop on Logic, Language, Information and Computation (WoLLIC11)
- Mathematical Logic in the Netherlands (MLNL09, MLNL10)
- Quantum Physics and Logic (QPL-11, QPL-12, QPL-13, QPL-14, QPL-15)
- Higher Dimensional Algebra, Categories and Types (HDACT)
- Computability and Complexity in Analysis (CCA08)
Organization: PhDay'01, Constructive mathematics, types and exact real numbers, DIAMANT-day '05,
Brouwer seminar (from 2004 to 2007), MAP07
The constructivenews-list.
Grants
2018-2021: AFOSR grant: Homotopy type theory and probabilistic computation,
540kUSD. The goal of the project is to apply homotopy type theory to
probabilistic programming and to develop theory and tools for computer
aided proofs in security.
2015-2019: 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.
Post-docs
Danil Annenkov
Sabine Oechsner
Evgeny Makarov (2013)
PhD-students
Benjamin Salling Hvass (2019-2022)
Jakob Botsch Nielsen (2019-2023)
Andreas Aagaard Lynge (2019-2022)
Soren Eller Thomsen (2018-2021)
Martin Bidlingmaier (2018-2021)
Russell O'Connor Incompleteness and Completeness Formalizing Logic and Analysis in Type Theory (2005-2008).
Research Assistants
Egbert Rijke (2012-2013).
Eelis van der Weegen (2010-2011).
Vacancies: we regularly have funding for PhD-students and postdocs. Please reach
out to me by
e-mail. The application
process goes via the graduate school.
Teaching
PGP