description

Name: CoRN
Title: Coq Repository at Nijmegen

Author: Evgeny Makarov
Author: Robbert Krebbers
Author: Eelis van der Weegen
Author: Bas Spitters
Author: Jelle Herold
Author: Russell O'Connor
Author: Cezary Kaliszyk
Author: Dan Synek
Author: Luís Cruz-Filipe
Author: Milad Niqui
Author: Iris Loeb
Author: Herman Geuvers
Author: Randy Pollack
Author: Freek Wiedijk
Author: Jan Zwanenburg
Author: Dimitri Hendriks
Author: Henk Barendregt
Author: Mariusz Giero
Author: Rik van Ginneken
Author: Dimitri Hendriks
Author: Sébastien Hinderer
Author: Bart Kirkels
Author: Pierre Letouzey
Author: Lionel Mamane
Author: Nickolay Shmyrev
Institution: Radboud University Nijmegen

Description:
 The Coq Repository at Nijmegen, CoRN, includes the following parts:

*  Algebraic Hierarchy

   o An axiomatic formalization of the most common algebraic
     structures, including setoids, monoids, groups, rings,
     fields, ordered fields, rings of polynomials, real and
     complex numbers

* Model of the Real Numbers

   o Construction of a concrete real number structure
     satisfying the previously defined axioms

* Fundamental Theorem of Algebra

   o A proof that every non-constant polynomial on the complex
     plane has at least one root

* Real Calculus

   o A collection of elementary results on real analysis,
     including continuity, differentiability, integration,
     Taylor's theorem and the Fundamental Theorem of Calculus

* Exact Real Computation
   o Fast verified computation inside Coq. This includes: real numbers, functions,
     integrals, graphs of functions, differential equations.

CoRN depends on the math-classes contribution. This mostly replaces the old algebraic hierarchy.

The author list is roughly in anti-chronological order.

URL: http://c-corn.cs.ru.nl
Keywords: constructive mathematics, algebra, real calculus, real numbers,
Fundamental Theorem of Algebra 
Category: Mathematics/Algebra
Category: Mathematics/Real Calculus and Topology
Category: Mathematics/Exact Real computation