Fri 12 Jan 2018 16:15 - 16:40 at Watercourt - Types for State Chair(s): Neel Krishnaswami

We provide a practical way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be recalled in the current state, provided (1) state evolves according to a given preorder, and (2) the property is preserved by this preorder. In many realistic scenarios, such monotonic reasoning yields concise modular proofs, saving the need for explicit program invariants. We distill our approach into the monotonic-state monad, a general yet compact interface for Hoare-style reasoning about monotonic state in a dependently typed language. We prove the soundness of the monotonic-state monad and use it as a unified foundation for reasoning about monotonic state in the F* verification system. Based on this foundation, we build libraries for various mutable data structures like monotonic references and apply these libraries at scale to the verification of several distributed applications.

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

15:50 - 17:05
Types for StateResearch Papers at Watercourt
Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge
15:50
25m
Talk
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Research Papers
Amin Timany imec-Distrinet KU-Leuven, Leo Stefanesco ENS Lyon, Morten Krogh-Jespersen Aarhus University, Lars Birkedal Aarhus University
16:15
25m
Talk
Recalling a Witness: Foundations and Applications of Monotonic State
Research Papers
Danel Ahman Inria Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris and ENS Paris, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
Pre-print
16:40
25m
Talk
RustBelt: Securing the Foundations of the Rust Programming Language
Research Papers
Ralf Jung MPI-SWS, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Robbert Krebbers Delft University of Technology, Derek Dreyer MPI-SWS