Interactive computer mathematics is a technology that interactively allows humans to learn, apply, develop, visualize and typeset mathematics. Eventually this should lead to the next generation of calculators and computer algebra systems, supporting a wide range of mathematical activities.

At the Brouwer Institute of Nijmegen University Barendregt's group works on languages, libraries and tools to bootstrap existing systems into the next generation. Thereby the calculus of inductive constructions (lambda calculus with dependent and inductive types) is used as the underlying logical system as implemented in the system Coq. This choice is based on the possibility to develop constructive proofs that provide algorithms for existential statements.

See as case studies the Fundamental Theorems of Algebra (every non-constant polynomial over the complex numbers has a zero) and Analysis (differentiation is the inverse of integration for continuous functions).

The project is relevant for the `Quest of Correctness'. This Quest decides whether the highest possible standard of correctness can be assigned to properties of mathematical models and their applications. These applications include tools used for construction and verification of software and systems.