<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Aptos;
panose-1:2 11 0 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:11.0pt;
mso-ligatures:none;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="color:black">Hi,<br>
<br>
On Monday, the MSP101 talk will be given by Clovis Eberhart (MSP). See the details of the talk below.<o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="color:black"><br>
Best,<br>
Dilsat<br>
<br>
**********************************************************************<br>
<br>
Date: Monday, 17 February at 15:00<br>
<br>
Room: LT1414a, Livingstone Tower<br>
<br>
Zoom link: <a href="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1" target="_blank" title="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1"><span style="color:#96607D">https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1</span></a><br>
<br>
Speaker: Clovis Eberhart<br>
<br>
Title: Weakest Precondition of Open Coalgebras<o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="color:black">Abstract: Coalgebras are a categorical framework that have proved useful to describe and reason about different types of systems. We define open coalgebras, a compositional framework where coalgebras can be composed as string diagrams.
We give them a semantics in terms of weakest precondition predicate transformers computed as a fixed point and link it to previous work on weakest precondition predicate transformers by Aguirre, Katsumara, and Kura. We give several examples of verification
problems this semantics can compute, showing its practical usefulness. We give conditions under which this semantics is compositional for the string diagram structure of open coalgebras. Finally, we give a syntactic precomputation of open coalgebras that removes
their internal states while preserving their semantics.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><br>
**********************************************************************<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>