[Prev][Next][Index][Thread]
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,
/R