C-CoRN, the Constructive Coq Repository at Nijmegen

We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain the structure, the contents and the use of the library. Moreover we discuss the motivation and the (possible) applications of such a library.

• Type: Conference
• Year: 2004
• Where: MKM
• Authors: Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk
• Keywords: Constructive Algebra, Constructive Coq Repository, MKM 2004, Theorem Prover Coq