Ryan Kavanagh : Order-theoretic Semantics for Recursive Session-Typed Processes

Vous pouvez consulter l’enregistrement de ce séminaire ici (durée : 1 huere).

Heure et date : le 15 octobre 2025 à 12h30
Lieu : PK-4610 et Zoom
Conférencier : Ryan Kavanagh

Titre : Order-theoretic Semantics for Recursive Session-Typed Processes

Résumé : Session-typed programming languages help programmers correctly implement communicating systems. Though many techniques exist for reasoning about these languages and their processes, few treat general recursive types, and few are compositional. As a consequence, they cannot be applied to many useful programs, and they do not support modular reasoning. In this talk, I will present a denotational semantics for Polarized Intuitionistic Processes (PIP), a session-typed proofs-as-processes interpretation of polarized intuitionistic linear logic. PIP features general recursion, channel transmission, choices, and synchronization. This semantics generalizes Kahn’s semantics for dataflow networks to support bidirectional, session-typed communication. It supports modular reasoning and validates expected program equivalences. Moreover, it is sound relative to barbed congruence (the canonical behavioural notion of process equivalence), and it is fully abstract in the absence of negative channel transmission. As a result, our semantics provides an intuitively reasonable account of session-typed communication and a foundation for reasoning about processes in more realistic session-typed languages.

Biographie : Ryan Kavanagh est professeur au Département d’informatique depuis décembre 2023. Ses intérêts de recherche sont les fondements logiques et mathématiques des systèmes concurrents, des langages de programmation et des systèmes quantiques.