Personal tools
You are here: Home Events Title: Triangulating Context Lemmas

Title: Triangulating Context Lemmas

— filed under:

Speaker: Ian Stark

  • Lab Lunch
When Feb 20, 2018
from 01:00 PM to 02:00 PM
Where Mini Forum 2 (MF2) Level 4
Add event to calendar vCal



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.

Document Actions