Séminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexity

Xavier LeroyCollège de FranceScience du logicielAnnée 2022-2023Structures de données persistantesSéminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexityThe talk gives a brief overview of our book "Functional Algorithms, Verified!" and its approach to verifying not just correctness but also running time of a large collection of functional algorithms. Then, two examples are presented in more detail: real time queues and double-ended queues that are implemented purely functionally with the help of stacks and whose operations have guaranteed constant running time.