Speaker: Norihiro Yamada, INESC-TEC 

Date: 17 May 2024, 14h30

Venue: Room B4009 (Seminar room of Mathematics Department) 

Online: https://videoconf-colibri.zoom.us/j/93344876599?pwd=ejkrZ3FpYkh0NE1YV3NCdGFMOGw3QT09

Abstract: In this talk, I present an overview of recent work on game semantics for PCF extended with algebraic effects. PCF is a higher-order functional programming language, which is Turing complete due to recursion. By its unique intensionality, game semantics provides PCF with denotational semantics that is fully abstract; i.e., it mathematically characterises the operational equivalence of terms in PCF. An algebraic effect is a computational effect described by an equational theory in universal algebra, and it subsumes a large class of computational effects such as (probabilistic) nondeterminism, states, and so on. For extending fully abstract game semantics for PCF to algebraic effects, the intensionality of game semantics conflicts with the extensionality of algebraic effects. I have overcome this dilemma by a novel categorical (and group-theoretic) construction that precisely identifies the morphisms in the game semantics forced so by a given equational theory, and established the first full abstraction result for algebraically effectful PCF. This is joint work with Renato Neves.