12.veebr, 14:00 ICT-315 "Embracing monotonicity in F*"
Tarkvarateaduse instituudi seminaril esmaspäeval, 12.02.2018 kell 14:00 esineb Danel Ahman (Inria Paris, Prantsusmaa) teemal "Embracing monotonicity in F*".
Seminar toimub ruumis ICT-315.
In this talk I will survey the key role that monotonicity plays in the dependently typed programming language F*, both for programming and 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.
(based on joint work with Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy)