Re: [isabelle] proving the substitution lemma




On Nov 7, 2007, at 1:19 PM, Moez A. Abdel-Gawad wrote:

Your thoughts?
PS: I was wondering if there is a Coq package and/or
project similar to the 'isabelle-nominal' ones.


Hi Moez,

If you're interested in what is possible with a "lightweight"
approach in this area, you may want to take at the following
paper.


[1] Engineering Formal Metatheory, by Brian Aydemir, Arthur
Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie
Weirich.  Available from
http://www.cis.upenn.edu/~baydemir/papers.shtml#AydCha+07a

This is a paper that will appear at POPL 2008 that focuses on a
particular style of locally nameless representation for
formalizing languages with binding.  (Coq code for the paper is
available through the link above.)  The style is lightweight in
that one could use it in a variety of proof assistants, e.g., Coq
and Isabelle, without any additional infrastructure.  The paper
also makes some comparisons with other first-order approaches,
including the Isabelle/Nominal package.


If you're interested in nominal techniques in Coq, I can mention
two other works (which Christian Urban has already pointed out
on the Isabelle lists).


[2] Nominal Reasoning Techniques in Coq, by Brian Aydemir, Aaron
Bohannon, and Stephanie Weirich.  Available from
http://www.cis.upenn.edu/~baydemir/nominal-reasoning-in-coq.html

This is not really a package like the Isabelle/Nominal package but
more a demonstration of what nominal reasoning might look like in
Coq.  In order to be practically useable, a similar amount of
infrastructure would be required in Coq as in Isabelle.


[3] A locally nameless solution to the POPLmark challenge, by
Xavier Leroy.  Available from
http://cristal.inria.fr/~xleroy/POPLmark/locally-nameless/

Leroy uses some nominal techniques in a locally-nameless setting
in Coq.


Cheers,
Brian




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.