The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Here are some relevant Coq libraries that I remember :

(my memory is probably biased)

https://github.com/fpottier/dblib

http://ropas.snu.ac.kr/gmeta/

http://www.lacl.fr/~polonowski/Develop/DBGen/dbgen.html

https://www.ps.uni-saarland.de/autosubst/

http://www.nuprl.org/html/CFGVLFMTP2014/

If you have any questions about the CFGV work, I'll be elated to answer them.

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Dec 9, 2014 at 9:58 AM, Harley Eades III <harley.eades AT gmail.com> wrote:

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