[Alta-Logic] Peripatetic talk this Wed.: Jonathan Galligher on rewriting

[Robin Cockett]

Place: ICT 616

Time: 3:30 pm Wed.  11th April

Speaker: Jonathan Gallagher

Title: Krivine's presentation of Tait and Martin-L\"{o}f's technique
for confluence proofs

Abstract:
The Church-Rosser theorem states that beta reduction (defined for the lambda
calculus) is a confluent relation.  Barendregt gives a very simple proof of
this theorem, which he attributes to Tait and Martin-L\"{o}f.  This proof also
generalizes easily to extensions of the lambda calculus.  In this talk, we
will review Tait and Martin-L\"{o}f's proof technique, and prove the confluence
of the lambda calculus.  We will then show how to use this proof technique to
prove that the differential lambda calculus is confluent.