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 (24)

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

This page was built for publication: Coquelicot: a user-friendly library of real analysis for Coq