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

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.


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.


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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.