Séminaire Cambium, Inria Paris, 2 rue Simone Iff Salle A215, bâtiment A Lundi 13 mars, 10h30 François Pottier Inria Paris Thunks and Debits in Iris with Time Credits A thunk is a mutable data structure that offers a simple memoization service: it stores either a suspended computation or the result of this computation. Okasaki (1999) presents many data structures that exploit thunks to achieve good amortized time complexity. He analyzes their complexity by associating a debt with every thunk. A debt can be paid off in several increments; a thunk whose debt has been fully paid off can be forced. Quite strikingly, a debt is associated also with future thunks, which do not yet exist in memory. Some of the debt of a faraway future thunk can be transferred to a nearer future thunk. In this talk, I will present a complete reconstruction of Okasaki's reasoning rules in Iris$, an extension of Iris with time credits. I will demonstrate the applicability of the rules by explaining how they can be used to verify a few operations on streams as well as one of Okasaki's data structures, namely the banker's queue. I will explain why reconstructing Okasaki's reasoning rules in Iris is nontrivial and will present a construction of the abstract predicate "Thunk" in three stages. The construction relies on a lower-level abstraction, the "piggy bank", a ghost data structure. This is joint work with Armaël Guéneau, Jacques-Henri Jourdan and Glen Mével. Vous pouvez vous abonner à nos annonces de séminaires: http://cambium.inria.fr/seminar.html Nos séminaires sont accessibles en ligne en direct: https://webconf.math.cnrs.fr/b/fra-ryy-fjn