This instance will be upgraded to Heptapod 0.25.0 (final) on 2021-09-22 at 15:00 UTC+2 (a few minutes of down time)

Commit a7dd6ef2 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

metadata for KAD; also added "depends-on = Kleene_Algebra" to KAT_and_DRA

parent 6a0a81f8963a
......@@ -1963,6 +1963,7 @@ abstract =
title = Kleene Algebra with Tests and Demonic Refinement Algebras
author = Alasdair Armstrong <http://www.dcs.shef.ac.uk/~alasdair>, Victor B. F. Gomes <http://www.dcs.shef.ac.uk/~victor>, Georg Struth <http://www.dcs.shef.ac.uk/~georg>
date = 2014-01-23
depends-on = Kleene_Algebra
topic = Computer Science/Programming Languages/Logics, Computer Science/Automata and Formal Languages, Mathematics/Algebra
abstract =
We formalise Kleene algebra with tests (KAT) and demonic refinement
......@@ -1977,9 +1978,10 @@ abstract =
[KAD]
title = Kleene Algebras with Domain
author = Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
author = Victor B. F. Gomes <http://www.dcs.shef.ac.uk/~victor>, Walter Guttmann, Peter Höfner <http://www.hoefner-online.de/>, Georg Struth <http://www.dcs.shef.ac.uk/~georg>, Tjark Weber <http://user.it.uu.se/~tjawe125/>
date = 2016-04-12
topic = Automata and Formal Languages; Programming Languages (Logics); Algebra
depends-on = Kleene_Algebra
topic = Computer Science/Programming Languages/Logics, Computer Science/Automata and Formal Languages, Mathematics/Algebra
abstract =
Kleene algebras with domain are Kleene algebras endowed with an
operation that maps each element of the algebra to its domain of
......
<!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">
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</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>&nbsp;</p>
<h1><font class="first">K</font>leene
<font class="first">A</font>lgebras
with
<font class="first">D</font>omain
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Kleene Algebras with Domain</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data"><a href="http://www.dcs.shef.ac.uk/~victor">Victor B. F. Gomes</a>, Walter Guttmann, <a href="http://www.hoefner-online.de/">Peter Höfner</a>, <a href="http://www.dcs.shef.ac.uk/~georg">Georg Struth</a> and <a href="http://user.it.uu.se/~tjawe125/">Tjark Weber</a></td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2016-04-12</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
Kleene algebras with domain are Kleene algebras endowed with an
operation that maps each element of the algebra to its domain of
definition (or its complement) in abstract fashion. They form a simple
algebraic basis for Hoare logics, dynamic logics or predicate
transformer semantics. We formalise a modular hierarchy of algebras
with domain and antidomain (domain complement) operations in
Isabelle/HOL that ranges from domain and antidomain semigroups to
modal Kleene algebras and divergence Kleene algebras. We link these
algebras with models of binary relations and program traces. We
include some examples from modal logics, termination and program
analysis.
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{KAD-AFP,
author = {Victor B. F. Gomes and Walter Guttmann and Peter Höfner and Georg Struth and Tjark Weber},
title = {Kleene Algebras with Domain},
journal = {Archive of Formal Proofs},
month = apr,
year = 2016,
note = {\url{http://afp.sf.net/entries/KAD.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Kleene_Algebra.shtml">Kleene_Algebra</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->
</tbody>
</table>
<p></p>
<!--#set var="name" value="KAD" -->
<!--#set var="binfo" value="../browser_info/current/AFP/${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>
</body>
</html>
......@@ -78,6 +78,10 @@ program verification tool prototype based on the algebraic approach.
<td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Kleene_Algebra.shtml">Kleene_Algebra</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
......@@ -49,6 +49,17 @@ A <a href="devel.shtml">development version</a> of the archive is available as w
<td class="head">2016</td>
</tr>
<tr><td class="entry">
2016-04-12:
<a href="entries/KAD.shtml">Kleene Algebras with Domain</a>
<br>Author:
<a href="http://www.dcs.shef.ac.uk/~victor">Victor B. F. Gomes</a>,
Walter Guttmann,
<a href="http://www.hoefner-online.de/">Peter Höfner</a>,
<a href="http://www.dcs.shef.ac.uk/~georg">Georg Struth</a> and
<a href="http://user.it.uu.se/~tjawe125/">Tjark Weber</a>
</td></tr>
<tr><td class="entry">
2016-03-11:
<a href="entries/PropResPI.shtml">Propositional Resolution and Prime Implicates Generation</a>
......
......@@ -47,6 +47,7 @@
<a href="entries/Tree-Automata.shtml">Tree-Automata</a> &nbsp;
<a href="entries/Kleene_Algebra.shtml">Kleene_Algebra</a> &nbsp;
<a href="entries/KAT_and_DRA.shtml">KAT_and_DRA</a> &nbsp;
<a href="entries/KAD.shtml">KAD</a> &nbsp;
<a href="entries/Regular_Algebras.shtml">Regular_Algebras</a> &nbsp;
<a href="entries/Markov_Models.shtml">Markov_Models</a> &nbsp;
<a href="entries/Probabilistic_System_Zoo.shtml">Probabilistic_System_Zoo</a> &nbsp;
......@@ -203,6 +204,7 @@
<a href="entries/Abstract-Hoare-Logics.shtml">Abstract-Hoare-Logics</a> &nbsp;
<a href="entries/Kleene_Algebra.shtml">Kleene_Algebra</a> &nbsp;
<a href="entries/KAT_and_DRA.shtml">KAT_and_DRA</a> &nbsp;
<a href="entries/KAD.shtml">KAD</a> &nbsp;
<a href="entries/BytecodeLogicJmlTypes.shtml">BytecodeLogicJmlTypes</a> &nbsp;
<a href="entries/DataRefinementIBP.shtml">DataRefinementIBP</a> &nbsp;
<a href="entries/RefinementReactive.shtml">RefinementReactive</a> &nbsp;
......@@ -318,6 +320,7 @@
<a href="entries/Matrix_Tensor.shtml">Matrix_Tensor</a> &nbsp;
<a href="entries/Kleene_Algebra.shtml">Kleene_Algebra</a> &nbsp;
<a href="entries/KAT_and_DRA.shtml">KAT_and_DRA</a> &nbsp;
<a href="entries/KAD.shtml">KAD</a> &nbsp;
<a href="entries/Regular_Algebras.shtml">Regular_Algebras</a> &nbsp;
<a href="entries/Free-Groups.shtml">Free-Groups</a> &nbsp;
<a href="entries/CofGroups.shtml">CofGroups</a> &nbsp;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment