|
 
|
[CFU08a] Deep-Embedded Unification
Rapport Scientifique : Date de dépot: 2008/01/01, (Tech. Rep.: CEDRIC-08-1547)Mots clés: unification, term algebra, proof assistant, deep embedding
Résumé:
We present some experiments with CiME/Coccinelle about standard first-order unification of deep-embedded terms in the Coq proof
assistant. We have modelled parts of the usual inference rules for
unification, namely Decompose, Merge and Coalesce as Coq functions and we proved their soundness and completeness. Regarding the Generalized Occur-Check, we use the CiME rewriting toolbox as an oracle either to provide a total ordering compatible with Occur-Check, or to exhibit a cycle. Then, using these informations, it is possible to prove in Coq that there is no most general unifier (mgu), or to compute it and prove that it actually enjoys the mgu properties. All together, it means that it is possible to compute an mgu for deep-embedded terms in Coq. This is a first step towards formal proofs of confluence for TRS.
Equipe:
sys
BibTeX
| @techreport { | |||
| CFU08a, | |||
| title | = | "{Deep-Embedded Unification}", | |
| author | = | "E. Contejean and J. Forest and X. Urbain", | |
| number | = | "{CEDRIC-08-1547}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {01-01-2008}, | |
| } | |||
