Real-Time Double-Ended Queue

Balazs Toth 📧 and Tobias Nipkow 🌐

June 23, 2022

Abstract

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.
BSD License

Topics

Theories of Real_Time_Deque