OREGON PROGRAMMING LANGUAGES SUMMER SCHOOL

https://www.cs.uoregon.edu/Research/summerschool/summer10/curriculum.html

The method of logical relations is a fundamental tool in type theory that is used to prove termination and normalization and to analyze equations between terms, including parametricity properties for polymorphism. The main idea is to interpret types as relations (of a suitable class) on terms by associating to each type constructor a "relational action" that determines the relation associated to a compound type as a function of its constituent types. The interpretation is chosen so that well-typed terms stand in the relation associated to their type, and so that related terms satisfy a property of interest, from which it follows that well-typed terms have that property. The method has many applications, but all share the characteristic that a global property of terms is reduced to local properties of types. I will develop the theory of logical relations from first principles, concentrating on two important cases, Goedel's System T and Girard's System F.

Shalom!

Lecture 1 first half he introduces Godels system B (a simple typed lambda caluclus with booleans) and shows that trying to prove termination by induction doesn't work because the induction hypothesis isn't strong enough to let us do

M1 M2 |-->* (\x:A, M) M2 --> [M2/x]M |-->? v

This motivates the Tate's fulcrum: strengthening induction from proving termination to reducibility, a concept we define recursively on the structure of types in order to make the proof work. The idea is to associate to each type a set of reducible terms.

>>2
Fuck off, illogical racist cretin.

>>4
>LLLLLLLLLLEEEEEEEEEEEEELLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLL
>LELLL
>LE NASTY END OF LE SHOTGUN
>LE ESSENTIAL RIGHTS
>EGIN

Furunculum on Tate's ass

>>5
Fuck off, freedom-hating cretin.

>>7
>LE EGIN SHOTGUN GRO