Triangulating context lemmas
Craig A. McLaughlin, James McKinna, Ian Stark · 2018
The idea of a context lemma spans a range of programming-language models: from Milner’s original through the CIU theorem to ‘CIU-like’ results for multiple language features. Each shows that to prove observational equivalence between program terms it is enough to test only some restricted class of contexts: applicative, evaluation, reduction, etc.