Mon 8 Jan 2018 16:00 - 16:30 at Museum A - Proof Methods and Libraries Chair(s): René Thiemann

The idea of a \emph{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, \textit{etc.}

We formally reconstruct a distinctive proof method for context lemmas based on cyclic inclusion of three program approximations: by triangulating between applicative' andlogical' 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.

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

16:00 - 18:00
Proof Methods and LibrariesCPP at Museum A
Chair(s): René Thiemann University of Innsbruck
16:00
30m
Talk
Triangulating Context Lemmas
CPP
Craig McLaughlin The University of Edinburgh, James McKinna , Ian Stark The University of Edinburgh
DOI
16:30
30m
Talk
Adapting Proof Automation to Adapt Proofs
CPP
Talia Ringer University of Washington, Nathaniel Yazdani University of Washington, Seattle, John Leo Halfaya Research, Dan Grossman University of Washington
DOI
17:00
30m
Talk
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
CPP
Niklas Grimm Vienna University of Technology, Austria, Kenji Maillard Inria Paris and ENS Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Matteo Maffei Saarland University, Jonathan Protzenko Microsoft Research, n.n., Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Santiago Zanella-Béguelin Microsoft Research, n.n.
DOI
17:30
30m
Talk
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
CPP
Hugo Férée University of Kent, UK, Samuel Hym University of Lille, France, Micaela Mayero , Jean-Yves Moyen University of Copenhagen, Denmark, David Nowak CNRS, France
DOI