Coquelicot: a user-friendly library of real analysis for Coq

DOI10.1007/s11786-014-0181-1zbMath1322.68176OpenAlexW1975906542MaRDI QIDQ2018661

Catherine Lelay, Guillaume Melquiond, Sylvie Boldo

Publication date: 25 March 2015

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-014-0181-1

zbMATH Keywords

differentiabilitypower seriesCoq proof assistantgeneralized limitslibraryparametric integralsstandard real analysis

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to real functions (26-04)

Related Items

A Formalization of Properties of Continuous Functions on Closed Intervals, Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL, Unnamed Item, Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis, Validating Mathematical Structures, Computational logic: its origins and applications, Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation, Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types, A Coq formalization of Lebesgue integration of nonnegative functions, Unnamed Item, Formalization of the Lindemann-Weierstrass theorem, A formal proof in Coq of Lasalle's invariance principle, Bellerophon: tactical theorem proving for hybrid systems, Formalising Mathematics in Simple Type Theory, Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method, Formally-verified round-off error analysis of Runge-Kutta methods, A Coq formalization of Lebesgue induction principle and Tonelli's theorem, Free modal Riesz spaces are Archimedean: a syntactic proof, Unnamed Item, The flow of ODEs: formalization of variational equation and Poincaré map, Formally verified approximations of definite integrals, Coquelicot, A Formal Proof of Cauchy’s Residue Theorem, Formally Verified Approximations of Definite Integrals

Uses Software

• ACL2
• Coq
• Isabelle/HOL
• PVS
• Mizar
• HOL Light
• C-CoRN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A computer-verified monadic functional implementation of the integral
• Constructing the real numbers in HOL
• The HOL Light theory of Euclidean space
• Formalization of Bernstein polynomials and applications to global optimization
• Formalization of real analysis: a survey of proof assistants and libraries
• HOL Light: An Overview
• A Brief Overview of Mizar
• A monadic, functional implementation of real numbers
• Proving Bounds on Real-Valued Functions with Computations
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Type classes for efficient exact real arithmetic in Coq
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Mathematical Knowledge Management
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Automated Deduction – CADE-20
• Nonstandard analysis in ACL2