Logical relations and the typed Lambda-calculus
Richard Statman
Discussion led by Fran Mota on March 4, 2016
This paper consists of the previously unpublished material from a course
of mine on the )t-calculus at Purdue in the spring of 1982.
PDF@ScienceDirectImportant note: This paper starts with lots of formalisms and gives lots of examples. The plan is to go through the examples during TPLS, please read at least the definitions beforehand!