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 Feb 20 2018 13.00 - 14.00 Lab Lunch: 20 February 2018 - Ian Stark Speaker: Ian Stark MF2 level 4
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 Feb 20 2018 13.00 - 14.00 Lab Lunch: 20 February 2018 - Ian Stark Speaker: Ian Stark MF2 level 4
