Axiomatisation d'un Lambda-Calcul avec Substitutions Explicites dans Coq
Abstract
Nous présentons l'axiomatisation de la théorie du $\Lenv$-calcul dans le système Coq. Le principal résultat axiomatisé est la confluence de ce calcul. Par ailleurs, nous proposons un codage uniforme des systèmes de réécriture à une ou plusieurs sortes, sur lequel nous étudions la confluence locale.