Email Gateway (Aug 18 2022 at 14:21): Email Gateway (Aug 18 2022 at 14:21):From: Tobias Nipkow <nipkow@in.tum.de>
We have two new and substantial contributions by Peter Lammich. His
Collections Framework is recommended to anyone who wants to generate
efficient code operating on sets, maps etc implemented as trees, hash
tables etc.
http://afp.sourceforge.net/entries/Collections.shtml
Collections Framework
This development provides an efficient, extensible, machine checked
collections framework. The library adopts the concepts of interface,
implementation and generic algorithm from object-oriented programming
and implements them in Isabelle/HOL. The framework features the use of
data refinement techniques to refine an abstract specification (using
high-level concepts like sets) to a more concrete implementation (using
collection data Twostructures, like red-black-trees). The code-generator
of Isabelle/HOL can be used to generate efficient code.
http://afp.sourceforge.net/entries/Tree-Automata.shtml
Tree Automata
This work presents a machine-checked tree automata library for
Standard-ML, OCaml and Haskell. The algorithms are efficient by using
appropriate data structures like RB-trees. The available algorithms for
non-deterministic automata include membership query, reduction,
intersection, union, and emptiness check with computation of a witness
for non-emptiness. The executable algorithms are derived from
less-concrete, non-executable algorithms using data-refinement
techniques. The concrete data structures are from the Isabelle
Collections Framework. Moreover, this work contains a formalization of
the class of tree-regular languages and its closure properties under set
operations.
Enjoy!
Tobias
Last updated: Nov 21 2024 at 12:39 UTC