swMATH ID: 6752
Software Authors: Henk Barendregt, Vince Bárány, Luís Cruz-Filipe, Herman Geuvers, Mariusz Giero, Rik van Ginneken, Dimitri Hendriks, Sébastien Hinderer, Cezary Kaliszyk, B. W. M. Kirkels, Pierre Letouzey, Iris Loeb, Lionel Mamanem Milad Niqui, Russell O’Connor, Randy Pollack, Nickolay V. Shmyrev, Bas Spitters, Dan Synek, Freek Wiedijk, Jan Zwanenburg
Description: 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.
Homepage: http://corn.cs.ru.nl/
Related Software: Coq; Mizar; Isabelle/HOL; HOL Light; ACL2; PVS; Isabelle; Whelp; Matita; Nuprl; kepler98; Coquelicot; OMDoc; ML; Isar; KeYmaera; Flocq; HOL; Proof General; AXIOM
Cited in: 41 Documents

Citations by Year