C-CoRN, the constructive Coq repository at Nijmegen

Abstract

We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a mathematical library of constructive algebra and analysis formalized in the theorem prover Coq. We explain the structure and the contents of the library and we discuss the motivation and some (possible) applications of such a library. The development of C-CoRN is part of a larger goal to design a computer system where 'a mathematician can do mathematics', which covers the activities of defining, computing and proving. An important proviso for such a system to be useful and attractive is the availability of a large structured library of mathematical results that people can consult and build on. C-CoRN wants to provide such a library, but it can also be seen as a case study in developing such a library of formalized mathematics and deriving its requirements. As the actual development of a library is very much a technical activity, the work on C-CoRN is tightly bound to the proof assistant Coq. © Springer-Verlag Berlin Heidelberg 2004.