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.