Speaker: Jonathan Gallagher
Title: Ditching squares for triangles — confluence in under an hour
Abstract: In this talk, we will give a proof of the Church-Rosser theorem for the lambda-calculus that is due to Takahashi 1995. Takashi used a property of developments — that they are always developing towards a ‘goal’ — to give the shortest known proof of confluence for the lambda calculus.
