[msp-interest] [MSP101] Clovis Eberhart: Weakest Precondition of Open Coalgebras (LT1414a, 3pm Mon 17-Feb)

[Dilsat Yuksel]

Hi,

On Monday, the MSP101 talk will be given by Clovis Eberhart (MSP). See the details of the talk below.

Best,
Dilsat

**********************************************************************

Date: Monday, 17 February at 15:00

Room: LT1414a, Livingstone Tower

Zoom link: https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1

Speaker: Clovis Eberhart

Title: Weakest Precondition of Open Coalgebras

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.

**********************************************************************

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20250213/3ad489a9/attachment.html