Coccinelle - Coccinelle
Date de dernière version : 01 janvier 2014

Responsable : CONTEJEAN Evelyne


Le but général de cette bibliothèque est d'utiliser le démonstrateur
automatique CiME pour produire des preuves en Coq, entre autres :

• d'égalité modulo dans une algèbre de termes quotient,
• de terminaison d'un système de réécriture,
• de confluence locale d'un tel système,
• de convergence.

Pour en savoir plus: http://www.lri.fr/~contejea/Coccinelle/coccinelle.html

Logiciel



Activités de recherche
  Démonstration automatique
  Réécriture

Membres
  CONTEJEAN Evelyne

Equipe
  Vérification d'Algorithmes, Langages et Systèmes

Equipe-projet Inria
  Toccata

TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas

BOLDR
Query Intermediate Representation Library