4 search results for "author:"guillaume.melquiond@inria.fr""

Showing 1 - 4

coq-coquelicot

No documentation

A Coq formalization of real analysis compatible with the standard library

keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and Topology logpath:Coquelicot date:2025-07-30

Sylvie Boldo <sylvie.boldo@inria.fr> Catherine Lelay <catherine.lelay@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>

3.4.4

LGPL-3.0-or-later

Used by 10 other packages

30 Jul 2025
coq-flocq

No documentation

A formalization of floating-point arithmetic for the Coq system

keyword:floating-point arithmetic logpath:Flocq date:2026-02-19

Sylvie Boldo <sylvie.boldo@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>

4.2.2

LGPL-3.0-or-later

Used by 18 other packages

19 Feb 2026
coq-gappa

No documentation

A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover

keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Gappa date:2026-02-19

Guillaume Melquiond <guillaume.melquiond@inria.fr>

1.8.0

LGPL-3.0-or-later

Used by 0 other packages

20 Feb 2026
coq-interval

No documentation

A Coq tactic for proving bounds on real-valued expressions automatically

keyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Calculus and Topology category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Interval date:2026-02-23

Guillaume Melquiond <guillaume.melquiond@inria.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr> Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>

4.11.4

CeCILL-C

Used by 8 other packages

23 Feb 2026