Coccinelle

Coccinelle

Évelyne Contejean


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 La méthodologie retenue est de produire des traces, mais il faut d'une part modéliser les propriétés à prouver dans Coq, d'autre part pour interpréter ces traces, il faut parfois prouver des propriétés sur les algorithmes sous-jacents. Par exemple, pour prouver la confluence locale d'un système de réécriture, il faut prouver que toutes les paires critiques sont confluentes. CiME va fournir une trace de réécriture des deux termes de chaque paire vers un réduit commun, mais il faut être sûr de vérifier toutes les paires critiques, et pour celà avoir une preuve de complétude de l'algorithme d'unification qui calcule ces paires.

Ce développement se veut donc une image en Coq du démonstrateur automatique CiME.

Table des modules actuellements présents1:

 list_extensions/ 
Résultats sur les listes, entre autres tri et permutation, utiles pour le cas multiset du rpo et le traitement de l'égalité modulo AC.

 term_algebra/ 


 term_orderings/ 


 ac_matching/ 
Définition de la théorie équationelle AC. Preuve du fait que l'égalité modulo AC est équivalente à l'égalité syntaxique des formes canoniques.

Définition d'un algorithme de matching modulo AC par règles d'inférence, preuve de sa terminaison, de sa complétude et de sa correction.

 unification/ 
Définition d'un algorithme d'unification syntaxique, preuve de sa terminaison, de sa complétude et de sa correction (en cours).


Documentation Lien sur l'archive


1
Ce développement est un travail en cours, il est donc amené à évoluer.

This document was translated from LATEX by HEVEA.