Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                            Lundi 25 avril, 10h30

                                  Glen Mével
                     Inria Paris & LMF, ENS Paris-Saclay

         Time debits in nested thunks: a proof of the banker's queue

By avoiding to compute the same thing twice, thunks are handy for
implementing persistent data structures with good amortized time
costs, regardless of their usage scenario. Okasaki’s “banker’s queue”
is one such data structure; it uses a lazy list.

Some program logics enable formal proofs of amortized time complexity
by means of a resource called “time credits”. In an earlier work, we
have shown how to construct time credits within Iris, thus enabling
time reasoning in a general-purpose program logic with separation. We
have demonstrated this by proving a specification for a library of
thunks, following Danielsson (2008). A thunk predicate has a time
debit to be paid before the thunk can be forced. However, our previous
work did not support anticipating debit from a nested thunk in an
enclosing thunk; we need this reasoning rule to prove the banker’s
queue. Thus, we present an updated API and proof for thunks, and we
sketch a proof of the correctness and amortized time complexity of the
banker’s queue.

            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