Lab Lunch: 20 February 2018 - Ian Stark

Title: Triangulating Context Lemmas

Abstract:

Craig McLaughlin, James McKinna and I published a paper last month about a  method for reasoning about equivalences between programs.  Craig gave a  technical talk at CPP 2018 (Certified Proofs and Programs); I'll present a  less formal overview of what our method does and what I like about it.  From the paper: 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  We formally reconstruct a distinctive proof method for context lemmas based on  cyclic inclusion of three program approximations: by triangulating between  'applicative' and 'logical' relations we prove that both match the  observational notion, while being simpler to compute.  Moreover, the  observational component of the triangle condenses a series of approximations  covering variation in the literature around what variable-capturing structure  qualifies as a 'context'.  Although entirely concrete, our approach involves no term dissection or  inspection of reduction sequences; instead we draw on previous context lemmas  using operational logical relations and biorthogonality.  We demonstrate the  method for a fine-grained call-by-value presentation of the simply-typed  lambda-calculus, and extend to a CIU result formulated with frame stacks.

https://dl.acm.org/citation.cfm?id=3167081