This is a verified implementation of a constant time queue. The original design is due to Hood and Melville. This formalization follows the presentation in Purely Functional Data Structuresby Okasaki.
- Hood, R., & Melville, R. (1981). Real-time queue operations in pure LISP. Information Processing Letters, 13(2), 50–54. https://doi.org/10.1016/0020-0190(81)90030-2