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
Type de document :
Mémoires d'étudiants -- Hal-inria+
Langage de programmation [cs.PL]. 2015
Liste complète des métadonnées

https://hal.inria.fr/hal-01250862
Contributeur : Matthieu Sozeau <>
Soumis le : mardi 5 janvier 2016 - 14:05:01
Dernière modification le : mercredi 20 janvier 2016 - 01:04:17
Document(s) archivé(s) le : jeudi 7 avril 2016 - 15:21:02

Identifiants

  • HAL Id : hal-01250862, version 1

Collections

Citation

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

Partager

Métriques

Consultations de
la notice

77

Téléchargements du document

38