[POPLmark] Re: [Provers] Re: adequacy

[Geoffrey A. Washburn]

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?

-- 
-- Geoff Washburn | geoffw at cis.upenn.edu | http://www.cis.upenn.edu/~geoffw/ --