4 search results for "author:"Érik Martin-Dorel""

Showing 1 - 4

coq-coqeal

No documentation

CoqEAL - The Coq Effective Algebra Library

category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:effective algebra keyword:elementary divisor rings keyword:Smith normal form keyword:mathematical components keyword:Bareiss keyword:Karatsuba multiplication keyword:refinements logpath:CoqEAL

Guillaume Cano Cyril Cohen Maxime Dénès Érik Martin-Dorel Anders Mörtberg et al.

2.1.2

MIT

Used by 4 other packages

24 Jul 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-09-16

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.5

CeCILL-C

Used by 11 other packages

16 Sep 2026
coq-libvalidsdp

No documentation

LibValidSDP

keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:libValidSDP

Pierre Roux <pierre.roux@onera.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr>

1.1.2

LGPL-2.1-or-later

Used by 2 other packages

23 Sep 2026
coq-validsdp

No documentation

ValidSDP

keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:ValidSDP

Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr>

1.1.2

LGPL-2.1-or-later

Used by 0 other packages

23 Sep 2026