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