This program is tentative and subject to change.

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.

This program is tentative and subject to change.

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Semantics 1POPL at Salon III
Chair(s): Alan Jeffrey Roblox
10:20
25m
Research paper
From Enhanced Coinduction towards Enhanced InductionRemote
POPL
Davide Sangiorgi University of Bologna
10:45
25m
Research paper
A Fine-Grained Computational Interpretation of Girard's Intuitionistic Proof-NetsInPerson?
POPL
Delia Kesner IRIF, France / University of Paris Diderot, France
11:10
25m
Research paper
Fully abstract models for effectful λ-calculi via category-theoretic logical relationsRemote
POPL
Philip Saville University of Oxford, Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics
11:35
25m
Research paper
Layered and Object-Based Game SemanticsInPerson
POPL
Arthur Oliveira Vale Yale University, Paul-André Melliès CNRS - Université de Paris, France, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS
Hide past events