Barendregt was right after all ... almost

Dear Colleague,

We are happy to announce the following two articles which might be of 
interest to the readers of the types and rewriting lists (and rush to 
apologise for multiple copies). Both are by Rene Vestergaard and James 
Brotherston and are available from 
http://iml.univ-mrs.fr/~vester/Writings/index.html. The articles are made 
available along with the associated Isabelle/HOL proof developments.

In one sense, the articles provide a formal justification for the use of 
the informal notion referred to as the Barendregt Variable Convention.

* A Formalised First-Order Confluence Proof for the lambda-Calculus Using 
One-Sorted Variable Names (Barendregt was right after all ... almost) --- 
to appear at RTA'01

* The Mechanisation of Barendregt-Style Equational Proofs (The Residual 
Perspective) --- preliminary version

We know of no other formal proof developments of equational properties that 
are conducted directly on first-order abstract syntax with one-sorted 
variable names (but are naturally interested in any pointers).

On behalf of the authors,