# Tree Automata

 Title: Tree Automata Author: Peter Lammich Submission date: 2009-11-25 Abstract: 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. BibTeX: @article{Tree-Automata-AFP, author = {Peter Lammich}, title = {Tree Automata}, journal = {Archive of Formal Proofs}, month = nov, year = 2009, note = {\url{https://isa-afp.org/entries/Tree-Automata.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Collections Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.