Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 2 new AFP entries: Collections and Tree Automata


view this post on Zulip 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: Mar 29 2024 at 12:28 UTC