Skip to Main content Skip to Navigation
Master thesis

Ensembles nominaux dans Coq/SSreflect

Gabriel Lewertowski 1, 2
1 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
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
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01250862
Contributor : Matthieu Sozeau <>
Submitted on : Tuesday, January 5, 2016 - 2:05:01 PM
Last modification on : Thursday, March 5, 2020 - 6:30:48 PM
Long-term archiving on: : Thursday, April 7, 2016 - 3:21:02 PM

Identifiers

  • HAL Id : hal-01250862, version 1

Collections

Citation

Gabriel Lewertowski. Ensembles nominaux dans Coq/SSreflect. Langage de programmation [cs.PL]. 2015. ⟨hal-01250862⟩

Share

Metrics

Record views

295

Files downloads

120