Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Real-Time Double-Ended Queue


view this post on Zulip Email Gateway (Jul 01 2022 at 07:06):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce a new AFP entry.

Real-Time Double-Ended Queue
by Balazs Toth and Tobias Nipkow

A double-ended queue (deque) is a queue where one can enqueue and
dequeue at both ends. We define and verify the deque implementation
by Chuang and Goldberg. It is purely functional and all operations
run in constant time.

https://www.isa-afp.org/entries/Real_Time_Deque.html

Enjoy,
René


Last updated: Mar 28 2024 at 12:29 UTC