Fri 21 Jan 2022 11:10 - 11:35 at Salon III - Semantics 1 Chair(s): Alan Jeffrey

We present a construction which, under suitable assumptions, takes a model of Moggi’s computational $\lambda$-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, $\top\top$-lifting, and $\top\top$-closure, takes inspiration from O’Hearn & Riecke’s fully abstract model for PCF. Our construction can be applied in the category of sets and functions, as well as the category of diffeological spaces and smooth maps and the category of quasi-Borel spaces, which have been studied as semantics for differentiable and probabilistic programming.

#### Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change

 10:20 - 12:00 Semantics 1POPL at Salon III Chair(s): Alan Jeffrey Roblox 10:2025mResearch paper From Enhanced Coinduction towards Enhanced InductionRemotePOPLDavide Sangiorgi University of Bologna; Inria DOI Media Attached 10:4525mResearch paper A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-NetsInPersonPOPLDelia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France DOI Media Attached 11:1025mResearch paper Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemotePOPLOhad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics, Philip Saville University of Oxford DOI Media Attached 11:3525mResearch paper Layered and Object-Based Game SemanticsInPersonPOPLArthur Oliveira Vale Yale University, Paul-André Melliès CNRS; Université de Paris, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS DOI Media Attached