HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

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.
Complete list of metadata

https://hal.inria.fr/inria-00123945
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Thursday, January 11, 2007 - 5:16:59 PM
Last modification on : Thursday, February 3, 2022 - 11:16:44 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 11:59:26 AM

Files

RR-6098.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

177

Files downloads

207