| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
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},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Collections |
| Status: [ok] | This is the development version, revision 4b34a59339a6, of this entry, generated for Isabelle revision 895d12fc0dd7. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|