Write a Blog >>
Mon 20 Jan 2020 10:51 - 11:13 at Maurepas - Program verification Chair(s): Nikhil Swamy

Braun trees are functional data structures for implementing extensible arrays and priority queues (and sorting functions based on the latter) efficiently. Some well-known functions on Braun trees have not yet been verified, including especially Okasaki’s linear time conversion from lists to Braun trees. We supply the missing proofs and verify all of these algorithms in Isabelle, including non-obvious time complexity claims. In particular we provide the first linear-time conversion from Braun trees to lists. We also state and verify a new characterization of Braun trees as the trees t whose index set is the interval {1, … size of t}.

Conference Day
Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Program verificationCPP at Maurepas
Chair(s): Nikhil SwamyMicrosoft Research
10:30
21m
Talk
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
CPP
Clement BlaudeauEcole Polytechnique, Natarajan ShankarSRI International, USA
DOI Pre-print Media Attached
10:51
22m
Talk
Proof Pearl: Braun Trees
CPP
Tobias NipkowTechnische Universität München, Thomas SewellChalmers University of Technology, Sweden
DOI Pre-print Media Attached
11:13
22m
Talk
FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP
Thomas LetanANSSI, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
DOI Pre-print Media Attached