Diff of /web/entries/Tree-Automata.shtml [000000] .. [1786b0]  Maximize  Restore

Switch to side-by-side view

--- a
+++ b/web/entries/Tree-Automata.shtml
@@ -0,0 +1,115 @@
+<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
+		"http://www.w3.org/TR/html4/loose.dtd">
+<html>
+<head>
+  <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">
+</head>
+<body>
+
+<table width="100%">
+  <tbody>
+    <tr>
+      <td width="20%" align="center" valign="top">
+      <!-- navigation -->
+      <!--#include file="nav.html"-->
+      </td>
+      <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">
+  <tbody>
+    <tr><td class="datahead" width="20%">Title:</td>
+    <td class="data" width="80%">
+<!-- Title: -->Tree Automata
+    </td></tr>
+		
+    <tr><td class="datahead">Author:</td>
+<td class="data">
+<!-- Author: -->Peter Lammich (peter lammich at uni-muenster de)
+</td></tr>		
+    
+	<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.
+
+   </td></tr>
+
+<!-- uncomment for entries significantly updated in devel version:
+<tr>
+<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>
+</tr> 
+-->
+
+<!--#set var="status" value="-STATUS-" -->
+<!--#set var="version" value="-VERSION-" -->
+<!---INCLUDE- file="devel-warning.shtml"-->
+</tbody>
+</table>
+
+<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">
+  <tbody>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="outline" -->">Proof outline</a><br>
+	<a href="<!--#echo var="doc" -->">Proof document</a>
+  </td>
+	<!-- link to README.hmtl if no document exists -->	
+	</tr>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="browse" -->">Browse theories</a>
+	</td></tr>
+    <tr>
+  <td class="links"> 
+	<a href="<!--#echo var="tar" -->">Download this entry</a>
+	</td>
+  </tr>
+    <tr><td class="links">Older releases:
+	None
+	</td></tr>
+  </tbody>
+</table>
+<!-- entry data end -->
+
+</td> </tr> </table>
+<div align="right" class="date">$Date: 2009-08-09 03:44:35 $, $Revision: 1.1 
+$</div></body>
+</html>

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks