BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Henning Basold (Universteit Leiden) DTSTART:20201014T140000Z DTEND:20201014T150000Z DTSTAMP:20260423T021129Z UID:OWLS/8 DESCRIPTION:Title: Coa lgebraic Communication Protocols and Session Types (YR-OWLS)\nby Henni ng Basold (Universteit Leiden) as part of Online Worldwide Seminar on Logi c and Semantics (OWLS)\n\n\nAbstract\nThis is joint work with Alex Keizer and Jorge A. Pérez.\n\nCompositional methods are central to the developme nt and verification of software systems. They allow to break down large sy stems into smaller components\, while enabling reasoning about the behavio ur of the composed system. For concurrent and communicating systems\, comp ositional techniques based on *behavioural type systems* have received muc h attention. By abstracting communication protocols as types\, these type systems can statically check that programs interact with channels accordin g to a certain protocol\, whether the intended messages are exchanged in a certain order. For this talk\, we will put on our coalgebraic spectacles to investigate *session types*\, a widely studied class of behavioral type systems. We will seek a syntax-free description of session-based concurre ncy as states of coalgebras. The result will be a description of type equi valence\, duality\, and subtyping relations in terms of canonical coinduct ive presentations. In turn\, this coinductive presentation makes it possib le to elegantly derive a decidable type system with subtyping for π-calcu lus processes\, in which the states of a coalgebra will serve as channel p rotocols. Going full circle\, we will also exhibit a coalgebra structure o n an existing session type system\, and show that the relations and type s ystem resulting from our coalgebraic perspective agree with the existing o nes.\n LOCATION:https://researchseminars.org/talk/OWLS/8/ END:VEVENT END:VCALENDAR