Coq.Interval - The Coq.Interval library for automatically proving bounds of real-valued expressions
Date of the last release: 15 September 2017

Person in charge : MELQUIOND Guillaume


The Coq.Interval library provides tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

More information: http://coq-interval.gforge.inria.fr/

Software - Licence : LGPL



Research activities

Members
  MELQUIOND Guillaume

Group
  Verification of Algorithms, Languages and Systems

Joint Inria project team
  Toccata

CODALAB
Codalab

DNADNA
Deep Neural Architectures for DNA

CARTOLABE
CARTOLABE