SourceForge has been redesigned. Learn more.

[1786b0]: / web / entries / Tree-Automata.shtml  Maximize  Restore  History

Download this file

116 lines (97 with data), 3.5 kB

<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
  <title>Archive of Formal Proofs</title>
  <link rel="stylesheet" type="text/css" href="front.css">
  <link rel="icon" href="../images/favicon.ico" type="image/icon">
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
  <meta name="GENERATOR" content="Quanta Plus">

<table width="100%">
      <td width="20%" align="center" valign="top">
      <!-- navigation -->
      <!--#include file="nav.html"-->
      <td width="80%" valign="top">
      <!-- content -->

<div align="center">
<p> </p>

<!-- begin entry data: -->
<h1><!-- Title: -->Tree Automata</h1>
<p> </p>

<table width="80%" class="data">
    <tr><td class="datahead" width="20%">Title:</td>
    <td class="data" width="80%">
<!-- Title: -->Tree Automata
    <tr><td class="datahead">Author:</td>
<td class="data">
<!-- Author: -->Peter Lammich (peter lammich at uni-muenster de)
	<tr><td class="datahead">Submission date:</td>
<td class="data"><!-- Submission date: -->2009-11-25</td></tr>

	<tr><td class="datahead" valign="top">Abstract:</td>
  <td class="abstract"> 
<!-- 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.


<!-- uncomment for entries significantly updated in devel version:
<td class="datahead"> </td>
<td class="data">An updated version of this entry is available in the 
    <a href="../download.shtml">development version</a> of AFP.</td>

<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->

<p> </p>

<!-- entry directory name: -->
<!--#set var="name" value="Tree-Automata" -->
<!--#set var="base" value="HOL" --> <!--- ??? could be HOLCF etc --->

<!--#set var="binfo" value="../browser_info/current/${base}/${name}" -->
<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->

<table class="links">
  <td class="links">
	<a href="<!--#echo var="outline" -->">Proof outline</a><br>
	<a href="<!--#echo var="doc" -->">Proof document</a>
	<!-- link to README.hmtl if no document exists -->	
  <td class="links">
	<a href="<!--#echo var="browse" -->">Browse theories</a>
  <td class="links"> 
	<a href="<!--#echo var="tar" -->">Download this entry</a>
    <tr><td class="links">Older releases:
<!-- entry data end -->

</td> </tr> </table>
<div align="right" class="date">$Date: 2009-08-09 03:44:35 $, $Revision: 1.1