Coq Repository at Nijmegen

The CoRN library has very roughly been developed in the following stages, chronologically:

• Fundamental Theorem of Algebra and the algebraic hierarchy. (Geuvers, Pollack, Wiedijk and Zwanenburg)
• Fundamental Theorem of Calculus, closely following the Bishop-Bridges book on Constructive Analysis. (PhD: Cruz-Filipe, advisor: Geuvers)
• Program extraction for real computation (Cruz-Filipe, Letouzey, Spitters)
• Abstract model of the real numbers (PhD: Niqui, advisor: Geuvers)
• Efficient computation with real numbers and metric spaces (PhD: O'Connor, advisor: Spitters)
• Riemann integration (O'Connor, Spitters)
• Interface with Coq's standard library reals (Kaliszyk, O'Connor).
• ForMath project (Spitters, Krebbers, van der Weegen, Makarov):
  • Fast computation inside Coq
  • Development of the math-classes library using type classes.
  • Development of a simple ODE-solver.