A locally nameless solution to the POPLmark challenge

Abstract : The POPLmark challenge is a collective experiment intended to assess the usability of theorem provers and proof assistants in the context of fundamental research on programming languages. In this report, we present a solution to the challenge, developed with the Coq proof assistant, and using the "locally nameless" presentation of terms with binders introduced by McKinna, Pollack, Gordon, and McBride.
Type de document :
Rapport
[Research Report] RR-6098, INRIA. 2007, pp.54
Liste complète des métadonnées

https://hal.inria.fr/inria-00123945
Contributeur : Rapport de Recherche Inria <>
Soumis le : jeudi 11 janvier 2007 - 17:16:59
Dernière modification le : samedi 17 septembre 2016 - 01:37:28
Document(s) archivé(s) le : mardi 21 septembre 2010 - 11:59:26

Fichiers

RR-6098.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00123945, version 2

Collections

Citation

Xavier Leroy. A locally nameless solution to the POPLmark challenge. [Research Report] RR-6098, INRIA. 2007, pp.54. 〈inria-00123945v2〉

Partager

Métriques

Consultations de
la notice

274

Téléchargements du document

131