[POPLmark] Meta-comment

[Christian Urban]

Dear Benjamin, dear Karl and dear All

Benjamin Pierce writes:

 > Moreover, so far we've only seen two concrete answers to the challenge, 
 > and there are a few other representation techniques out there that also 
 > seem extremely promising -- for example, Christian Urban's nominal approach
 > and Michael Norrish's method based on the Gordon-Melham axioms.  

Many thanks for the nice words and high expectations. However the 
Twelf solution has set the mark very high and so I rather like to 
make the presentation of the nominal approach as clean as possible 
before circulating the results widely. This means not before Stefan 
Berghofer and I have implemented a new datatype package for Isabelle. 
So please be patient. 

BTW, the GM-5-axioms approach is not incompatible with the nominal
approach. Michael Norrish has happily married both, and his and my
approaches are extremely close so that we share many ideas and concepts. 
The only important ingredient one needs for a 'nominal approach' 
is to work with alpha-equivalence classes. The GM-5-axioms approach does 
provide a datatype for alpha-equivalence classes, but so does Peter 
Homeier's quotient-package, for example. 

Karl Crary writes:

 > I don't mean any disrespect to other systems when I say that to my 
 > knowledge no other system has demonstrated that it is ready for such 
 > use.  (I would be happy to be disproved on this point.)

Your are building here on the shoulders of Elf- and Twelf-giants who
already look back on more than 10 years of development. So, before you
declare the Twelf-solution as winner ;o), please give the others some time 
to sort out implementation issues. After all, only slightly more than 
a half a year ago we found out that an implementation of nominal sets 
is in fact possible in Isabelle/HOL.

Regards,
Christian