POPL 2022 (series) / POPL Research Papers / Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemote
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
Fri 21 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mResearch paper | From Enhanced Coinduction towards Enhanced InductionRemote POPL Davide Sangiorgi University of Bologna; Inria DOI Media Attached | ||
10:45 25mResearch paper | A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-NetsInPerson POPL Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France DOI Media Attached | ||
11:10 25mResearch paper | Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemote POPL Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics, Philip Saville University of Oxford DOI Media Attached | ||
11:35 25mResearch paper | Layered and Object-Based Game SemanticsInPerson POPL Arthur 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 |