¶
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