[POPLmark] Re: [Provers] Re: adequacy

[Karl Crary]

Yes, that should definitely be done eventually.  Carsten and I have been 
thinking about the best way to do it, but it's not at all on the fast track.

    -- Karl


Geoffrey A. Washburn wrote:

>On Thu, 5 May 2005, Karl Crary wrote:
>
>  
>
>>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.
>>    
>>
>
>	So maybe the question to ask is whether the formal system that
>  encompasses all of this meta-logical reasoning can be mechanized.
>  My guess is that there is no reason it couldn't.  But is it possible
>  that in some hypothetical future version of Twelf will I be able obtain
>  a proof term from the termination or coverage checkers?
>
>  
>