Skip to content
Snippets Groups Projects
Commit a438ca29 authored by Luigi Santocanale's avatar Luigi Santocanale
Browse files

modified: index.html

parent f9140e0d
No related branches found
No related tags found
No related merge requests found
...@@ -485,7 +485,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt ...@@ -485,7 +485,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
<tr style="background-color:#fafcff", valign="top"> <tr style="background-color:#fafcff", valign="top">
<td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T08:00:00">9:00</a></td> <td align="right"><a href="http://www.timeanddate.com/worldclock/fixedtime.html?iso=2021-11-03T08:00:00">9:00</a></td>
<td align="left"><i >Callum Bannister, Peter Höfner and <u >Georg Struth</u></i></td> <td align="left"><i ><u >Callum Bannister</u>, Peter Höfner and Georg Struth</i></td>
<td align="left", width="60%"> <td align="left", width="60%">
<a href="javascript:toggleDiv('T13')">Effect Algebras, Girard Quantales and Complementation in Separation Logic</a> <a href="javascript:toggleDiv('T13')">Effect Algebras, Girard Quantales and Complementation in Separation Logic</a>
<div style="display:none", id="T13"><br /><br />We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. This shows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.</div> <div style="display:none", id="T13"><br /><br />We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. This shows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.</div>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment