This page needs updating.
2015: Associate professor at CMU working on the MURI grant Homotopy Type Theory: Unified Foundations of Mathematics and Computation
- Constructive mathematics: type theory and topos theory
- Computer mathematics, interactive theorem proving
- Logical and categorical foundations of physics
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.)
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
- 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, QPL-15)
- Higher Dimensional Algebra, Categories and Types (HDACT)
- Certified Programs and Proofs (CPP13)
- Calculemus 15
Homotopy Type Theory and Univalent Foundations - Mini-Symposium at DMV 2015.
CIRM workshop: Computable Analysis: Foundations, Implementation and Certification.
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).
Onderwijs Seminar on simplicial methods (2012)