C-CoRN
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.
Keywords for this software
References in zbMATH (referenced in 33 articles , 1 standard article )
Showing results 1 to 20 of 33.
Sorted by year (- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
- Li, Wenda; Paulson, Lawrence C.: A formal proof of Cauchy’s residue theorem (2016)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: a user-friendly library of real analysis for Coq (2015)
- Krebbers, Robbert; Spitters, Bas: Type classes for efficient exact real arithmetic in Coq (2013)
- Makarov, Evgeny; Spitters, Bas: The Picard algorithm for ordinary differential equations in Coq (2013)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Improving real analysis in Coq: a user-friendly approach to integrals and derivatives (2012)
- Alama, Jesse; Brink, Kasper; Mamane, Lionel; Urban, Josef: Large formal wikis: issues and solutions (2011)
- Bertot, Yves; Guilhot, Frédérique; Mahboubi, Assia: A formal study of Bernstein coefficients and polynomials (2011)
- Paşca, Ioana: Formal proofs for theoretical properties of Newton’s method (2011)
- Spitters, Bas; van der Weegen, Eelis: Type classes for mathematics in type theory (2011)
- Geuvers, Herman; Koprowski, Adam; Synek, Dan; van der Weegen, Eelis: Automated machine-checked hybrid system safety proofs (2010)
- O’Connor, Russell; Spitters, Bas: A computer-verified monadic functional implementation of the integral (2010)
- Spitters, Bas; van der Weegen, Eelis: Developing the algebraic hierarchy with type classes in Coq (2010)
- Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman: A Wiki for Mizar: motivation, considerations, and initial prototype (2010)
- Biha, Sidi Ould: Finite groups representation theory with Coq (2009)
- Geuvers, H.: Proof assistants: history, ideas and future (2009)
- Julien, Nicolas; Paşca, Ioana: Formal verification of exact computations using Newton’s method (2009)
- Rioboo, Renaud: Invariants for the FoCaL language (2009)
- Kaliszyk, Cezary: Automating side conditions in formalized partial functions (2008)
- O’Connor, Russell: Certified exact transcendental real number computation in Coq (2008)