Triangulating context lemmas

Craig McIaughlin, James McKinna, Ian D. B. Stark

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

3 Citations (Scopus)

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 languageEnglish
Title of host publicationCPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
PublisherAssociation for Computing Machinery
Pages102-114
Number of pages13
ISBN (Electronic)9781450355865
DOIs
Publication statusPublished - 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

    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