Abstract
The idea of a context lemma spans a range of programminglanguage models: from Milner’s original through the CIU theorem to ‘CIUlike’ 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 variablecapturing 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 finegrained callbyvalue presentation of the simplytyped lambdacalculus, 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 welltyped and wellscoped 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.
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 variablecapturing 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 finegrained callbyvalue presentation of the simplytyped lambdacalculus, 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 welltyped and wellscoped 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 language  English 

Title of host publication  Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs 
Place of Publication  New York, NY, USA 
Publisher  ACM 
Pages  102114 
Number of pages  13 
ISBN (Print)  9781450355865 
DOIs  
Publication status  Published  8 Jan 2018 
Event  7th ACM SIGPLAN International Conference on Certified Programs and Proofs  Los Angeles, United States Duration: 8 Jan 2018 → 9 Jan 2018 https://popl18.sigplan.org/track/CPP2018 
Publication series
Name  CPP 2018 

Publisher  ACM 
Conference
Conference  7th ACM SIGPLAN International Conference on Certified Programs and Proofs 

Abbreviated title  CPP 2018 
Country  United States 
City  Los Angeles 
Period  8/01/18 → 9/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.Profiles

Ian Stark
 School of Informatics  Senior Lecturer
 Laboratory for Foundations of Computer Science
 Foundations of Computation
Person: Academic: Research Active