Xavier Leroy. A locally nameless solution to the POPLmark challenge. Research report 6098, INRIA, January 2007.

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.

bib | Local copy | At publisher's ] Back

This file was generated by bibtex2html 1.97.