Iowa Type Theory Commute
Start of discussion on how to prove confluence for untyped lambda calculus. Also some discussion about the research community interested in confluence.