Document Open Access Logo

Real-Time Double-Ended Queue Verified (Proof Pearl)

Authors Balazs Toth, Tobias Nipkow

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2023.29.pdf
  • Filesize: 0.63 MB
  • 18 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Balazs Toth
  • Department of Computer Science, Technische Univerität München, Germany
Tobias Nipkow
  • Department of Computer Science, Technische Univerität München, Germany

Funding

  • Nipkow, Tobias: Research partially supported by DFG Koselleck grant NI 491/16-1.

References

  1. 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.
  2. 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.
  3. 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. Google Scholar
  4. Alejandro Gómez-Londoño. Hood-Melville queue. Archive of Formal Proofs, January 2021. URL: https://isa-afp.org/entries/Hood_Melville_Queue.html.
  5. 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. Google Scholar
  6. Robert Hood. The Efficient Implementation of Very-High-Level Programming Language Constructs. PhD thesis, Cornell University, 1982. TR 82-503. Google Scholar
  7. 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.
  8. 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.
  9. 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.
  10. Tobias Nipkow, editor. Functional Data Structures and Algorithms. A Proof Assistant Approach. Forthcoming. URL: https://functional-algorithms-verified.org/.
  11. Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
  12. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  13. 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.
  14. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact