[POPLmark] Meta-comment

[Peter Sewell]

Karl>I believe that we demonstrate Twelf's practicality by the fact that we 
Karl>use it for nearly all of our work at CMU, and, so you don't have to take 
Karl>our word for it, by the fact that we were able to solve the Poplmark 
Karl>challenge without much difficulty.

Indeed, and it's impressive, and I'm not disputing it at all.  I was
simply observing that "for our work at CMU" is a crucial point - the
fact that it works great for you is very informative but is not the
whole answer.  I have the impression that the kind of metatheory you
do fits particularly well with the intended Twelf style.  Other things
seem not to, and it's not clear (at least to this non-expert) where
the boundary is.  The example I mentioned is a case where some
"traditional" PL metatheory, which would fit well, has to be combined
with a lot of operational modelling that wouldn't.  For another (open)
case, one could think of work making heavy use of structural
congruences and coinductive operational reasoning. 

best,
Peter