Coquelicot: a user-friendly library of real analysis for Coq
From MaRDI portal
Publication:2018661
DOI10.1007/S11786-014-0181-1zbMATH Open1322.68176OpenAlexW1975906542MaRDI QIDQ2018661FDOQ2018661
Authors: Sylvie Boldo, Catherine Lelay, Guillaume Melquiond 
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
Recommendations
differentiabilitypower seriesCoq proof assistantgeneralized limitslibraryparametric integralsstandard real analysis
Cites Work
- A Brief Overview of Mizar
- Mathematical Knowledge Management
- Verified Real Number Calculations: A Library for Interval Arithmetic
- Formalization of real analysis: a survey of proof assistants and libraries
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Formalization of Bernstein polynomials and applications to global optimization
- HOL Light: An Overview
- Proving Bounds on Real-Valued Functions with Computations
- Automated Deduction – CADE-20
- The HOL Light theory of Euclidean space
- Title not available (Why is that?)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Title not available (Why is that?)
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Nonstandard analysis in ACL2
- A computer-verified monadic functional implementation of the integral
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Constructing the real numbers in HOL
- Title not available (Why is that?)
- Computing with classical real numbers
- A monadic, functional implementation of real numbers
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
Cited In (29)
- \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
- A framework for formal verification of robot kinematics
- A formalization of properties of continuous functions on closed intervals
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- A formal proof of Cauchy's residue theorem
- A Coq formalization of Lebesgue integration of nonnegative functions
- Computable analysis and notions of continuity in \textsc{Coq}
- Formally-verified round-off error analysis of Runge-Kutta methods
- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
- The flow of ODEs: formalization of variational equation and Poincaré map
- Formalising Mathematics in Simple Type Theory
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- 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
- Formally verified approximations of definite integrals
- Formally verified approximations of definite integrals
- Coquelicot
- Formalization techniques for asymptotic reasoning in classical analysis
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Validating Mathematical Structures
- A Coq formalization of Lebesgue induction principle and Tonelli's theorem
- Computational logic: its origins and applications
- Formalization of real analysis: a survey of proof assistants and libraries
- Formalization of the Lindemann-Weierstrass theorem
- Free modal Riesz spaces are Archimedean: a syntactic proof
- A formal proof in Coq of Lasalle's invariance principle
- Bellerophon: tactical theorem proving for hybrid systems
- Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
- Canonical Big Operators
Uses Software
This page was built for publication: Coquelicot: a user-friendly library of real analysis for Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2018661)
