I lead the Nijmegen contribution to the ForMath project, as well as Work Package 4: formalization of exact analysis. (The project got an "excellent" mark.)
- Constructive mathematics and its foundations (type theory, formal topology, topos theory...)
- Computer mathematics (combining proving and computing in one integrated computer environment)
- Logical and categorical foundations of physics.
2013: Member of the Institute for Advanced Studies for the special year on univalent foundations.
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.
- 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)
- 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)
- Higher Dimensional Algebra, Categories and Types (HDACT)
- Certified Programs and Proofs (CPP13)
Previous grants: VENI `Reasoning and Computing' of the dutch science foundation NWO.
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).