Constructive Coq Repository at Nijmegen

Foundations Group, Radboud University Nijmegen

Hello, these pages are a bit outdated; you can find the latest source code on

Latest Stable Revision: here (works with Coq 8.4)

Feel free to ask question through email or on the #coq IRC channel on freenode.

Also see the math-classes project.

The Constructive Coq Repository at Nijmegen, C-CoRN, aims at building a computer based library of constructive mathematics, formalized in the theorem prover Coq.

Background There is a lot of mathematical knowledge. This knowledge is mainly stored in books and in the heads of mathematicians and other scientists. Putting this knowledge in the right form on a computer, the mathematics should be more readily available to be used by others (either humans or other computer applications). C-CoRN aims at being a starting point and a test-bed for this: we put mathematics on a computer in an active (formalized) way to see how one can interact with it (consult, use, extend) and how to manage it (document, update, keep consistent). The reason for working constructively is partly historical, partly practical (because we wanted to use Coq, which is a constructive theorem prover), but mainly because constructive mathematics has the additional bonus of providing (actual, executable) algorithms for the functions that we prove to exist. C-CoRN grew out of the FTA project, formalizing the Fundamental Theorem of Algebra. (See the history page for an overview and links.) The repository is developed and maintained by the Foundations Group of the NIII (Computer Science Department) of the University of Nijmegen, but everybody is cordially invited to participate in its further development.

Why Computer formalized mathematics has a high potential: a good computer-representation of mathematics will enable the following.

An important condition for opening up these potential advantages of formalized mathematics is having an extensive formalized library of (basic) results. C-CoRN aims at being such a library. In the context of our work, this library serves several purposes.

What We formalize constructive mathematics in Coq. See the library for an overview. Currently we have: a Constructive Algebraic Hierarchy (up to the reals), a theory of Metric Spaces and Compact Subsets of complete metric spaces, an Effective Model of the Real Numbers, a proof of the Fundamental Theorem of Algebra and the Fundamental Theorem of Calculus, and the ability to generate plots of uniformly continuous functions.

Who See the people page to see who has contributed to C-CoRN.

Home [History] [People] [On-line Documentation] [Publications] [Library] [Download] [Contact Information]