[POPLmark] Re: [Provers] Re: adequacy

[Karl Crary]

If I recall correctly, Schuermann's thesis is the canonical source for 
the coverage checker, but not for the termination checker, which would 
be covered by Brigitte Pientka's PhD thesis.  Also, Schuermann's thesis 
presents things in a slightly different form than the one used 
externally by Twelf.

I would say that the source for all this is the Twelf manual, together 
with the copious collection of examples that accompany the 
distribution.  A more succinct resource would be a tutorial that was 
part of my paper on foundational certified code.  (The version on my web 
page is old, but the tutorial hasn't changed much.)  As mentioned, Bob 
and I are finishing up a note on adequacy and the interpretation of 
meta-proofs.

Uniqueness checking is not currently part of Twelf, and has nothing that 
I know of to do with the current discussion.

    -- Karl


Geoffrey A. Washburn wrote:

>On Thu, 5 May 2005, Robert Harper wrote:
>
>  
>
>>Contrary to what you're suggesting, there already IS a single source for
>>this, namely Schuermann's PhD thesis.
>>    
>>
>
>	I wasn't aware that his thesis covered the details for uniqueness
>  checking, for example.
>
>  
>