### Abstract

The idea of a context lemma spans a range of programminglanguage 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 simplytyped lambda-calculus, and extend to a CIU result formulated with frame stacks. All this is formalised and proved in Agda: building on work of Allais et al., we exploit dependent types to specify lambdacalculus terms as well-typed and well-scoped by construction. By doing so, we seek to dispel any lingering anxieties about the manipulation of concrete contexts when reasoning about bound variables, capturing substitution, and observational equivalences. © 2018 Copyright held by the owner/author(s). Publication rights licensed to the Association for Computing Machinery.

Original language | English |
---|---|

Title of host publication | CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs |

Publisher | Association for Computing Machinery |

Pages | 102-114 |

Number of pages | 13 |

ISBN (Electronic) | 9781450355865 |

DOIs | |

Publication status | Published - 8 Jan 2018 |

### Keywords

- Agda
- CIU theorem
- Context lemma
- Dependent types
- Logical relations
- Observational equivalence
- Calculations
- Concretes
- Differentiation (calculus)
- Software testing
- Observational equivalences
- Equivalence classes

## Fingerprint Dive into the research topics of 'Triangulating context lemmas'. Together they form a unique fingerprint.

## Profiles

## James McKinna

- School of Mathematical & Computer Sciences - Associate Professor
- School of Mathematical & Computer Sciences, Computer Science - Associate Professor

Person: Academic (Research & Teaching)

## Cite this

McIaughlin, C., McKinna, J., & Stark, I. D. B. (2018). Triangulating context lemmas. In

*CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs*(pp. 102-114). Association for Computing Machinery. https://doi.org/10.1145/3167081