Fran├žais Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software Coq
Coq - The Coq proof assistant
Date of the last release: 17 February 2018

Person in charge : MELQUIOND Guillaume


Coq provides both a dependently-typed functional programming language and a logical formalism, which, altogether, support the formalisation of mathematical theories and the specification and certification of properties of programs. Coq also provides a large and extensible set of automatic or semi-automatic proof methods. Coq's programs are extractible to OCaml, Haskell, Scheme, ...

More information: https://coq.inria.fr/

Software



Research activities

Members
  FILLI├éTRE Jean-Christophe
  PAULIN-MOHRING Christine
  MELQUIOND Guillaume

Group
  Verification of Algorithms, Languages and Systems

Joint Inria project team
  Toccata
Software & patents
TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas

BOLDR
Query Intermediate Representation Library