Logical Relations

A devious technique for performing induction over types. Can be used for a number of purposes:

to prove properties of programming languages
to quotient at higher types, thereby constructing extensional models
...

References