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.
  author  = {Peter Lammich},
  title   = {Tree Automata},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2009,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Collections