Triangulating Context Lemmas

Craig McLaughlin, James McKinna, Ian Stark

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

All this is formalised and proved in Agda: building on work of Allais et al., we exploit dependent types to specify lambda-calculus 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.
Original languageEnglish
Title of host publicationProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Place of PublicationNew York, NY, USA
PublisherACM
Pages102-114
Number of pages13
ISBN (Print)978-1-4503-5586-5
DOIs
Publication statusPublished - 8 Jan 2018
Event7th ACM SIGPLAN International Conference on Certified Programs and Proofs - Los Angeles, United States
Duration: 8 Jan 20189 Jan 2018
https://popl18.sigplan.org/track/CPP-2018

Publication series

NameCPP 2018
PublisherACM

Conference

Conference7th ACM SIGPLAN International Conference on Certified Programs and Proofs
Abbreviated titleCPP 2018
CountryUnited States
CityLos Angeles
Period8/01/189/01/18
Internet address

Keywords

  • Agda
  • CIU theorem
  • Context lemma
  • Dependent types
  • Logical relations
  • Observational equivalence

Fingerprint

Dive into the research topics of 'Triangulating Context Lemmas'. Together they form a unique fingerprint.

Cite this