Real-Time Double-Ended Queue

Balazs Toth 📧 and Tobias Nipkow 🌐

June 23, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


Related publications

  • Chuang, T.-R., & Goldberg, B. (1993). Real-time deques, multihead Turing machines, and purely functional programming. Proceedings of the Conference on Functional Programming Languages and Computer Architecture - FPCA ’93.
  • Wikipedia

Session Real_Time_Deque