Title	Confluence of untyped lambda calculus via simple types
Authors	Silvia Ghilezan, Computing Science Department, Catholic University Viktor Kuncak, Laboratory of Computer Science, MIT
Main Fields	21. type theory
Other Main Fields	lambda calculus
Abstract + Keywords	We present a new proof of confluence of the untyped lambda calculus by embedding untyped lambda terms into simply typed lambda terms. This embedding allows us to define a reduction on all lambda terms, whose transitive closure is the beta reduction, using an auxiliary reduction and the beta reduction on simply typed lambda terms. The confluence of the auxiliary reduction makes explicit the joining of the sets of redexes to be  reduced. This embedding allows us to use the confluence of beta reduction on simply typed lambda terms and thus prove the confluence of the reduction defined. As a consequence we obtain the confluence of beta reduction  in theuntyped lambda calculus.