The Mechanisation of Barendregt-Style Equational Proofs

(The Residual Perspective)

Authors: Rene Vestergaard and James Brotherston

The Isabelle theories below comprise the Isabelle / HOL implementation of the proof of the results in section 3 of the the article. All proofs are due to the authors. Queries or comments are naturally welcome and may be directed either to Rene Vestergaard or James Brotherston.

View theory dependencies