Fran├žais Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software Flocq Library
Flocq Library - Flocq Library
Date of the last release: 10 January 2014

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/

Software - Licence : LGPL



Research activities
  Program proof
  Floating-point arithmetic

Members
  BOLDO Sylvie
  MELQUIOND Guillaume

Group
  Verification of Algorithms, Languages and Systems

Joint Inria project team
  Toccata
Software & patents
DNADNA
Deep Neural Networks for DNA

TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas