SourceForge.net Logo
project summary

 

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{http://afp.sf.net/entries/Tree-Automata.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Collections