The Nijmegen group works on foundations of type systems and on formalization of mathematics on proof development systems.
Milena Stefanova completed a model construction of the calculus of constructions with parametric inductive types, showing strong normalization and hence consistency of this system in a modular way. Henk Barendregt and Erik Barendsen described a general technique replacing proofs by computations (which do not require deduction steps).
Mark Ruys formalized algebraic concepts in Lego, including construction of the field of complex numbers. Towards a formalized proof of the Fundamental Theorem of Algebra, he showed the existence of k-th roots in the complex numbers. Further case studies include a constructive proof of the binomial theorem. Barendregt and Barendsen currently investigate the applicability of the `proofs by computation' approach in various areas of mathematics, including reasoning about continuity and extensionality. The method involves an explicit inductive formalization of mathematical expressions. Another running project is the construction of a compiler from Lego to Coq in collaboration with R. Maron (University of Warsaw).