×

C-CoRN, the constructive Coq repository at Nijmegen. (English) Zbl 1108.68586

Asperti, Andrea (ed.) et al., Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19–21, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23029-7/pbk). Lecture Notes in Computer Science 3119, 88-103 (2004).
Summary: 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.
For the entire collection see [Zbl 1053.68003].

MSC:

68T30 Knowledge representation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Coq; C-CoRN; Nuprl; Theorema; OMDoc
PDFBibTeX XMLCite
Full Text: DOI