[POPLmark] Re: [Provers] Re: adequacy

[Brigitte Pientka]

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.
>

I would like to correct that my PhD thesis covers the termination checker.
In my thesis, I describe different techniques to improve the overall
performance and the expressive power of higher-order logic programming
within Twelf. The motivating question is the same spirit as posed in
Challenge 3 of Poplmark: what technology is needed to be able to execute,
experiment with and "animate" specifications of formal systems.

My work on the termination checker for Twelf was independent of my thesis
and is explained in the paper "Verifying termination and reduction
properties about higher-order logic programs" which will be published as
part of a special issue on termination in the Journal of Automated
Reasoning. A preliminary version is available of my web-site.

Best,

- Brigitte Pientka