Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

Nijmegen

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

• Mathematical libraries and repositories. (Collaboration with INRIA Sophia-Antipolis, INRIA-Futurs, Orsay, Bologna, Biaystok.)
• Formalizing constructive and exact analysis as a case study, but also in relation to the computational aspects of mathematics. (Collaboration with Göteborg, INRIA Sophia-Antipolis)
• Closing the gap between formal and informal mathematical proofs, (Collaboration with Biaystok, Bologna, INRIA Sophia-Antipolis)
• Proof presentation: how to present a formalized proof in an (interactive) document, e.g. on the web.(Collaboration with Bologna, INRIA Sophia-Antipolis)
• Interactive theorem proving: how to (formally) model the interaction between a mathematician and a theorem proving system and how to present an unfinished proof in an understandable way and to interact with it. (Collaboration with Biaystok, Bologna, INRIA Sophia-Antipolis, INRIA Futurs)
• Write an overview book on typed lambda calculus. (Collaboration with Torino, Udine, INRIA Futurs, Bergen)

The senior members of the Foundations group are

• Herman Geuvers, contact person
• Henk Barendregt
• Jan Willem Klop
• Rob Nederpelt from TU Eindhoven
• Wil Dekkers
• Freek Wiedijk
• Bas Spitters

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