I had the chance to follow Goubault-Larrecq's very nice course on Logic and Computation, that went over this in a very similar way. Unfortunately, the whole mat

I had the chance to follow Goubault-Larrecq's very nice course on Logic and Computation, that went over this in a very similar way. Unfortunately, the whole material is in french, but might still interest some : http://www.lsv.fr/~goubault/Lambda/loginfoindex.html http://www.lsv.fr/~goubault/Lambda/loginfoindex.html (The relevant part is the "Lambda calcul pur" one")