LIPIcs.ITP.2023.29.pdf
- Filesize: 0.63 MB
- 18 pages
Document
Real-Time Double-Ended Queue Verified (Proof Pearl)
Authors
Tobias Nipkow 
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Cite AsGet BibTex
Balazs Toth and Tobias Nipkow. Real-Time Double-Ended Queue Verified (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.29
https://doi.org/10.4230/LIPIcs.ITP.2023.29
Abstract
We present the first verification of the real-time doubled-ended queue by Chuang and Goldberg where all operations take constant time. The main contributions are the full system invariant, the precise definition of all abstraction functions, the structure of the proof and the main lemmas.
Subject Classification
ACM Subject Classification
- Software and its engineering → Formal software verification
- Theory of computation → Data structures design and analysis
- Software and its engineering → Functional languages
Keywords
- Double-ended queue
- data structures
- verification
- Isabelle
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- F. Warren Burton. An efficient functional implementation of FIFO queues. Inf. Process. Lett., 14(5):205-206, 1982. URL: https://doi.org/10.1016/0020-0190(82)90015-1.
- Tyng-Ruey Chuang and Benjamin Goldberg. Real-time deques, multihead turing machines, and purely functional programming. In Functional programming languages and computer architecture - FPCA quotesingle93. ACM Press, 1993. URL: https://doi.org/10.1145/165180.165225.
-
Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, European Symposium on Programming (ESOP 2013), volume 7792 of LNCS, pages 125-128. Springer, 2013.
- Alejandro Gómez-Londoño. Hood-Melville queue. Archive of Formal Proofs, January 2021. URL: https://isa-afp.org/entries/Hood_Melville_Queue.html.
-
Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, Functional and Logic Programming (FLOPS 2010), volume 6009 of LNCS, pages 103-117. Springer, 2010.
-
Robert Hood. The Efficient Implementation of Very-High-Level Programming Language Constructs. PhD thesis, Cornell University, 1982. TR 82-503.
- Robert Hood and Robert Melville. Real-time queue operation in pure LISP. Inf. Process. Lett., 13(2):50-54, 1981. URL: https://doi.org/10.1016/0020-0190(81)90030-2.
- Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. Contract-based resource verification for higher-order functions with memoization. In Giuseppe Castagna and Andrew D. Gordon, editors, Symposium on Principles of Programming Languages, POPL 2017, pages 330-343. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009874.
- Ravichandhran Madhavan and Viktor Kuncak. Symbolic resource bound inference for functional programs. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification, CAV 2014, volume 8559 of LNCS, pages 762-778. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_51.
- Tobias Nipkow, editor. Functional Data Structures and Algorithms. A Proof Assistant Approach. Forthcoming. URL: https://functional-algorithms-verified.org/.
- Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
-
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
- Chris Okasaki. Simple and efficient purely functional queues and deques. J. Funct. Program., 5(4):583-592, 1995. URL: https://doi.org/10.1017/S0956796800001489.
- Balazs Toth and Tobias Nipkow. Real-time double-ended queue. Archive of Formal Proofs, June 2022. , Formal proof development. URL: https://www.isa-afp.org/entries/Real_Time_Deque.html.