Next: Nottingham
Up: Cooperating sites
Previous: TU Munich


The Foundations group of the Computer Science Department has a long history and expertise in (1) lambda calculus, (2) type theory and its relation to logic, and (3) formalizing mathematics, especially in type theory based systems, but also in more general. The group has completed a full formalization of (a constructive proof of) the Fundamental Theorem of Algebra (FTA) and the Fundamental Theorem of Calculus (FTC) in Coq. This formalization is continuously extended and updated, thus creating a large mathematical repository. The groups members are knowledgeable Coq users but also have expertise in Mizar and HOL-light. Furthermore the group has a great expertise in constructive logic and mathematics.

The team will mainly contribute to the objective of Formal Mathematics and Mathematics Education and to a lesser extent to Proof Technology and Foundational Studies. Currently, the group's main focuses are

The senior members of the Foundations group are

Our research on Formalizing Mathematics is partially funded by a national ``Spinoza'' grant of Barendregt for outstanding researchers. The research on proof presentation and closing the gap between formal and informal mathematics is partially funded by the Calculemus EC-TMR and partially by the IST-FET project MoWGLI.

Nijmegen homepage

Bengt Nordström 2005-09-22