Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Sun 3 Sep 2017 16:50 - 17:20 at L3 - Monotonicity

In this talk we discuss our work on techniques to aid the verification of programs whose state evolves monotonically according to a preorder (a reflexive, transitive relation). We give a formal account of a useful verification model: a property witnessed at some state s0 can be safely recalled at any future state s1, so long as the state evolves monotonically and that property is stable with respect to the given preorder. Specifically, we study this style of verification in the context of the effectful dependently typed programming language F*. While specific instances of this verification model are used extensively in F*, their use has been somewhat ad hoc so far. In this work we provide a general framework for this style of verification: we develop a preorder-respecting version of F*’s state effect, equip it with an instrumented operational semantics, and demonstrate how the instances of this verification model already used in F* can be implemented in our general framework.

Sun 3 Sep

Displayed time zone: Belfast change

16:50 - 17:40
MonotonicityHOPE at L3
Recalling a Witness
Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, n.n., Cédric Fournet Microsoft Research, n.n.