### 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

BSD License

### Topics

- Computer science/Data structures

### 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

## Cite

×

Real_Time_Deque-AFP

    @article{Real_Time_Deque-AFP,
      author  = {Balazs Toth and Tobias Nipkow},
      title   = {Real-Time Double-Ended Queue},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Real_Time_Deque.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jul 1, 2022 : Isabelle2021-1
- Jun 30, 2022 : Isabelle2021-1