Flocq Library - Flocq Library


Person in charge : BOLDO Sylvie


Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.

More information: http://flocq.gforge.inria.fr/

- Licence : LGPL



Research activities
  Program proof
  Floating-point arithmetic

Members
  BOLDO Sylvie
  MELQUIOND Guillaume

Group
  Verification of Algorithms, Languages and Systems

BSP++
The C++ Bulk Synchronous Parallelism Library

TAXOMAP ALIGNMENT
A prototype to automate semantic mappings between taxonomies

FR1155729
Procédé pour l’extinction de routeurs dans un réseau de communications et routeur mettant en œuvre ce procédé