CoRN
A Coq library for constructive real analysis and algebra, including a model of real numbers and exact real computation.
What is CoRN?
C-CoRN is a Coq library that formalizes constructive real analysis and algebra, providing a verified framework for reasoning about real numbers, algebraic structures, and calculus. It solves the problem of ensuring mathematical correctness in computational mathematics by offering formally proven results and enabling exact real computation within Coq.
Researchers and developers working in formal verification, constructive mathematics, or theorem proving who need a reliable library for real analysis and algebra in Coq.
Developers choose C-CoRN for its comprehensive, constructively verified approach to real analysis and algebra, unique integration of exact real computation, and strong foundation in Coq's proof assistant ecosystem.
Overview
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
Use Cases
Best For
- Formally verifying properties of real numbers and algebraic structures
- Conducting constructive mathematics research with Coq
Related Projects
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
