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.
License
Topics
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. https://doi.org/10.1145/165180.165225
- Wikipedia
Session Real_Time_Deque
- Deque
- Type_Classes
- Stack
- Current
- Idle
- Common
- Big
- Small
- States
- RealTimeDeque
- Stack_Aux
- Current_Aux
- Idle_Aux
- Common_Aux
- Big_Aux
- Small_Aux
- States_Aux
- RealTimeDeque_Aux
- RTD_Util
- Stack_Proof
- Idle_Proof
- Current_Proof
- Common_Proof
- Big_Proof
- Small_Proof
- States_Proof
- RealTimeDeque_Dequeue_Proof
- RealTimeDeque_Enqueue_Proof
- RealTimeDeque_Proof