\documentclass{article}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{mathpartir}
\usepackage{url}
\pagestyle{plain}
\usepackage{color,colortbl}
\usepackage{hevea}

\loadcssfile{../styles/style.css}


\title{Coccinelle}
\author{\ahref{\url{http://www.lri.fr/~contejea/introduction_fr}}{\'Evelyne Contejean}}
\newcommand{\CiME}{C\textit{i}ME}

\begin{document}
\begin{center}
\begin{rawhtml}
<img src="./coccinelle2_104.png" alt="Coccinelle" border="0">
<H3 CLASS="titlerest"><A HREF="http://www.lri.fr/~contejea/introduction_fr">\'Evelyne Contejean</A>
\end{rawhtml}
\end{center}

\begin{rawhtml}
<link rel="shortcut icon" href="http://www.lri.fr/~contejea/Coccinelle/coccinelle2_32.ico" />
\end{rawhtml}

%\maketitle


Le but g\'en\'eral de cette biblioth\`eque est d'utiliser le d\'emonstrateur
automatique \ahref{http://cime.lri.fr}{\CiME{}} pour produire des
preuves en Coq, entre autres 
\begin{itemize}
\item d'\'egalit\'e modulo dans une alg\`ebre de termes
quotient, 
\item de terminaison d'un syst\`eme de r\'e\'ecriture,
\item de confluence locale d'un tel syst\`eme, 
\item de convergence.
\end{itemize}

La m\'ethodologie retenue est de produire des traces, mais il faut
d'une part mod\'eliser les propri\'et\'es \`a prouver dans Coq, d'autre part pour
interpr\'eter ces traces, il faut parfois prouver des propri\'et\'es sur 
les algorithmes sous-jacents. Par exemple, pour prouver la confluence
locale d'un syst\`eme de r\'e\'ecriture, il faut prouver que toutes les
paires critiques sont confluentes. \CiME{} va fournir une trace de
r\'e\'ecriture des deux termes de chaque paire vers un r\'eduit commun,  
mais il faut \^etre s\^ur de v\'erifier {\em toutes} les paires critiques,
et pour cel\`a avoir une {\em preuve de compl\'etude de l'algorithme
d'unification} qui calcule ces paires.

Ce d\'eveloppement se veut donc une image en Coq du d\'emonstrateur automatique 
\CiME. 

Table des modules actuellements pr\'esents\footnote{Ce d\'eveloppement est
un travail en cours, il est donc amen\'e \`a \'evoluer.}:

\definecolor{gold}{rgb}{1,0.843,0}
\definecolor{orangered}{rgb}{1,0.271,0}
\definecolor{chocolate}{rgb}{0.824,0.412,0.118}
\definecolor{deeppink3}{rgb}{0.804,0.063,0.463}
\definecolor{crimson}{rgb}{0.863,0.078,0.235}


\begin{description}
\item[\colorbox{gold}{~list\_extensions/~}]
 R\'esultats sur les listes, entre autres tri et permutation, utiles
  pour le cas multiset du rpo et le traitement de l'\'egalit\'e modulo AC.

 
\item[\colorbox{orangered}{~term\_algebra/~}]
\begin{itemize}
\item D\'efinition d'alg\`ebres de termes g\'en\'eriques (sur une signature 
   arbitraire), des terms, sous-terms, substitutions, bonne formation,
    taille, divers principes d'induction sur les termes.
\item \'Egalit\'e / r\'e\'ecriture modulo un ensemble d'axiomes
\end{itemize}

\item[\colorbox{chocolate}{~term\_orderings/~}]
\begin{itemize}
  \item Definition d'un ordre total sans propri\'et\'es additionelles,
  utile pour mettre les termes modulo AC dans une forme canonique.
  \item Rpo. 
D\'efinition inductive du rpo avec status pour les termes
 g\'en\'eriques.
    preuves que rpo est un pr\'eordre
    preuves de monotonicit\'e, stabilit\'e par instanciation
    preuves d'accessibilit\'e si la pr\'ec\'edence sous-jacente est bien
 fond\'ee.
\end{itemize}

\item[\colorbox{deeppink3}{~ac\_matching/~}]
D\'efinition de la th\'eorie \'equationelle AC. Preuve du fait que l'\'egalit\'e
modulo AC est \'equivalente \`a l'\'egalit\'e syntaxique des formes
canoniques.

D\'efinition d'un algorithme de matching modulo AC par r\`egles
d'inf\'erence, preuve de sa terminaison, de sa compl\'etude et de sa correction.

\item[\colorbox{crimson}{~unification/~}]
D\'efinition d'un algorithme d'unification syntaxique, preuve de sa
terminaison, de sa compl\'etude et de sa correction (en cours).

\end{description}


\rawhtmlinput{graph.html}


\ahref{\url{http://www.lri.fr/~contejea/Coccinelle/doc}}{Documentation}
\ahref{\url{http://www.lri.fr/~contejea/Coccinelle/coccinelle.tgz}}{Lien sur l'archive}
\ahref{\url{http://www.lri.fr/~contejea/Coccinelle/coccinelle83pl4.tgz}}{New : a
  revised version which compiles with Coq v8.3pl4}

\end{document}