TY - GEN
T1 - Verified Analysis of Functional Data Structures
AU - Nipkow, Tobias
N1 - Publisher Copyright:
© 2020 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.
PY - 2016/6/1
Y1 - 2016/6/1
N2 - In recent work the author has analyzed a number of classical functional search tree and priority queue implementations with the help of the theorem prover Isabelle/HOL. The functional correctness proofs of AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees could be automated. The amortized logarithmic complexity of skew heaps, splay trees, splay heaps and pairing heaps had to be proved manually.
AB - In recent work the author has analyzed a number of classical functional search tree and priority queue implementations with the help of the theorem prover Isabelle/HOL. The functional correctness proofs of AVL trees, red-black trees, 2-3 trees, 2-3-4 trees, 1-2 brother trees, AA trees and splay trees could be automated. The amortized logarithmic complexity of skew heaps, splay trees, splay heaps and pairing heaps had to be proved manually.
KW - Algorithm Analysis
KW - Functional Programming
KW - Program Verification
UR - http://www.scopus.com/inward/record.url?scp=85120092637&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSCD.2016.4
DO - 10.4230/LIPIcs.FSCD.2016.4
M3 - Conference contribution
AN - SCOPUS:85120092637
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
A2 - Kesner, Delia
A2 - Pientka, Brigitte
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Y2 - 22 June 2016 through 26 June 2016
ER -