Viðburðir eftir árum


ICE-TCS seminar: Danel Ahman

Embracing monotonicity in F*

  • 29.1.2018, 12:10 - 13:00

ICE-TCS-logo-200px

Date and time: Monday, 29 January 2018 from 12:10 till 13:00
Place: Room M1.11 at Reykjavik University

Title: Embracing monotonicity in F*

Speaker:  Danel Ahman (INRIA Paris Rocquencourt)

Abstract
In this talk, I will survey the key role that monotonicity plays in the dependently typed programming language F*, both for programming and for verification. First, I will present a monotonic variant of F*'s global state effect that captures the following idea: a property witnessed in a prior state can be soundly recalled in the current state, provided (1) state evolves according to a given preorder, and (2) the property is preserved by this preorder. Next, I will present some example uses of this notion of monotonicity, ranging from basic examples (such as monotonic counters), to advanced examples (such as heap-based memory models supporting both untyped and (monotonic) typed references), to some more involved case studies. Finally, I will present a small dependently typed effectful lambda calculus in which we formalise the above intuitions and prove them correct. If time permits, I will also discuss the challenges arising when adding support for monadic reification for such monotonic-state computations, so as to prove relational properties of such programs, e.g., noninterference.

This is based on joint work with Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy.

You can read an interview with Danel at  

http://www.cs.cmu.edu/~popl-interviews/ahman.html