The Coq mailing list

[Harley Eades III <harley.eades AT gmail.com>]

Hi, Gergely.

One way to represent binders is called the Locally Nameless representation.  I find this to be

the easiest to use personally.

You will find the original paper here:

http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf

You might also enjoy this blog post:

http://math.andrej.com/2012/11/29/how-to-implement-dependent-type-theory-iii/

Very best,

.\ Harley

On Dec 9, 2014, at 9:41 AM, Gergely Buday <gbuday AT gmail.com> wrote:

Hi there,

what is the current state of the art of formalising languages with
binders using Coq? What are the classic papers on this?

- Gergely