[POPLmark] how to believe a twelf proof

Robert Harper rwh at cs.cmu.edu
Mon May 9 16:43:13 EDT 2005


In response to the recent discussion on the POPLmark challenge mailing 
list, we have decided to write a brief note entitled "How To Believe a 
Twelf Proof" that summarizes the key ideas underlying the Twelf 
meta-theorem prover, which we used extensively in our solution to the 
POPLmark challenge.  The note is not intended as a guide to using the 
Twelf system, but rather as an exposition of the underlying concepts 
that appear to have caused some confusion.

Bob Harper and Karl Crary


-------------- next part --------------
A non-text attachment was scrubbed...
Name: believe-twelf.pdf
Type: application/pdf
Size: 139648 bytes
Desc: not available
Url : http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050509/a215ec69/believe-twelf-0001.pdf


More information about the Poplmark mailing list