A Formalised First-Order Confluence Proof for the Lambda-Calculus using One-Sorted Variable Names

(Barendregt was right after all ... almost)

Authors: Rene Vestergaard and James Brotherston



The Isabelle theories below comprise the entire Isabelle / HOL implementation of the titular proof development as given in the article. All proofs are due to the authors, with the exception of the proofs in the Commutation theory, for which we thank Tobias Nipkow. Queries or comments are naturally welcome and may be directed either to Rene Vestergaard or James Brotherston.


View theory dependencies



Isabelle / HOL Theories

High-level:

Mid-level:

Low-level: