Ensembles nominaux dans Coq/SSreflect
Résumé
Dans ce travail, on s’intéresse aux ensembles nominaux, un formalisme pour représenter
les variables liées introduit par Andrew Pitts [Pit13]. Son principal avantage est qu’il permet de raisonner dans des assistants de preuves formelles comme on le ferait informellement avec un papier, sans recourir à des manipulations techniques (décalages d’indices, ...) qui augmentent le risque d’erreurs.
Cette approche a été implémentée dans l’assistant de preuve Isabelle [Urb05] et a permis de prouver plusieurs résultats intéressants : théorème de Church-Rosser, Normalisation forte du lambda- calcul simplement typé, première partie du POPLmark Challenge [Ayd05].
Plusieurs tentatives ont ́et ́e faites pour d ́evelopper les mˆemes outils dans Coq, la plus aboutie date de 2006 [ABW06] et permet d’utiliser l’approche nominale pour raisonner sur le lambda-calcul, sans toutefois permettre `a l’utilisateur de d ́efinir des fonctions par r ́ecurrence sur les termes.
Dans ce rapport, on propose une formalisation des ensembles nominaux dans Coq qui permet
— De représenter un langage de programmation quelconque fourni par l’utilisateur. La partie 3
traite le cas de F<:, le langage étudié dans le POPLmark Challenge.
— De raisonner par induction en supposant qu’une variable liée est distincte d’un contexte donné
— De définir des fonctions récursives grâce à un combinateur
Loading...