I really like the exposition in http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf, but they do not have any solutions to the problems.

Am finding https://www.cs.ox.ac.uk/andrew.ker/docs/lambdacalculus-lecture-notes-ht2009.pdf a bit harder to follow, but they do have solutions to computational problems.

Thanks in advance!