A locally nameless solution to the POPLmark challenge

Xavier Leroy (1)

1 GALLIUM - Programming languages, types, compilation and proofs

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.

Mots clés: POPLmark; Coq; locally nameless; alpha-conversion; binders; type systems; metatheory; system F-sub

Domaines: Langage de programmation [cs.PL]; Logique en informatique [cs.LO]

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