[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Adam Chlipala]

Daniel C. Wang wrote:

>I had an idea for a relatively simple but artificial problem.
>
I've written a solution in Coq and put it on the web at:
    http://www.cs.berkeley.edu/~adamc/lamheight/

I interpreted the problem statement with the apparent corrections found 
in Michael Norrish's earlier reply.

I've used the most obvious encoding of variable binding.  The problem 
almost seems "unfair" because a solution needn't prove any "semantic" 
theorems, so the choice of binding mechanisms probably has little 
(positive!) effect on how easy it is to complete the challenge.  At any 
rate, this can serve at least as a baseline solution.  It's not long, 
I've tried to comment it so as to be understandable to non-Coq experts, 
and the link above includes a pretty-printed HTML version with comments 
(via coqdoc).