[POPLmark] Re: [Provers] Re: adequacy

[Geoffrey A. Washburn]

On Thu, 5 May 2005, Kevin Watkins wrote:

> If I were just starting to learn Twelf, I would focus on understanding
> what a Twelf proof (total function) is, first, before trying to
> understand Twelf's totality checker, or the messages it generates.

	In my experience it is simply not possible to understand what
  Twelf considers a proof without trying to understand the coverage
  checker.  For example, if I write down the obvious total function
  corresponding to a proof of about the type soundness of small step
  semantics, it will fail because Twelf does not perform splitting when
  considering output coverage.  Maybe this should be considered a bug in
  Twelf; Karl has argued otherwise in the past.  The point is that just
  writing down a total function in Twelf may not lead to a verifiable
  proof unless you understand the coverage checker.

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