Coquelicot: a user-friendly library of real analysis for Coq
type: Item
instance of: scholarly article
title: Coquelicot: a user-friendly library of real analysis for Coq
zbMATH Open document ID: 1322.68176
author: Sylvie Boldo
author: Catherine Lelay
author: Guillaume Melquiond
published in: Mathematics in Computer Science
publication date: 2015-03-25T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 26-04
zbMATH DE Number: 6419297
zbMATH Keywords: standard real analysis
zbMATH Keywords: Coq proof assistant
zbMATH Keywords: library
zbMATH Keywords: generalized limits
zbMATH Keywords: differentiability
zbMATH Keywords: parametric integrals
zbMATH Keywords: power series
describes a project that uses: Mizar
describes a project that uses: ACL2
describes a project that uses: C-CoRN
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: PVS
describes a project that uses: HOL Light
MaRDI profile type: Publication
full work available at URL: s11786-014-0181-1
OpenAlex ID: W1975906542
cites work: A monadic, functional implementation of real numbers
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
cites work: Wave equation numerical resolution: a comprehensive mechanized proof of a C program
cites work: Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
cites work: Formalization of real analysis: a survey of proof assistants and libraries
cites work: Mathematical Knowledge Management
cites work: Q4435465
cites work: Verified Real Number Calculations: A Library for Interval Arithmetic
cites work: Q2754041
cites work: Nonstandard analysis in ACL2
cites work: Q4736391
cites work: Constructing the real numbers in HOL
cites work: HOL Light: An Overview
cites work: The HOL Light theory of Euclidean space
cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
cites work: Q3184782
cites work: Type classes for efficient exact real arithmetic in Coq
cites work: Automated Deduction – CADE-20
cites work: Proving Bounds on Real-Valued Functions with Computations
cites work: Formalization of Bernstein polynomials and applications to global optimization
cites work: A Brief Overview of Mizar
cites work: A computer-verified monadic functional implementation of the integral
DOI: 10.1007/S11786-014-0181-1
description: scientific article; zbMATH DE number 6419297