[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Dimitrios Vytiniotis]

Hi, here's a small Isabelle/HOL script:

    www.cis.upenn.edu/~dimitriv/poplmark/DWang.thy

I can't say I agree that this example is a good test, in my opinion
*real* problematic examples, are those where the programmer ends up saying:

 Good God! not a 100th auxiliary lemma about my Stupid binders!!! (1)

and the particular example is way easier. With respect to integration of
theories of let's say Naturals or co-algebraic types, I believe---but
have not big experience---that all modern tools are quite good at that
already, no? Who isn't?

The real issue is of course that of extensibility of a representation
technique when new types have to be added or new reasoning methods have
to be used. A representation technique is no good when your 4-lemma
paper proof has to involve 40 auxiliary formal proofs *each* time you
want to use your representation. But evaluating that again requires many
real-world examples as test-cases because for examples in the scale
of the one Dan proposed we just can't say much (also read: I will never
reach mental state (1) above).

Best,
-dimitris