Stream: Mirror: Isabelle Users Mailing List

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

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: Jan 04 2025 at 20:18 UTC