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

There exist a rich and well-developed theory of enhancements of the coinduction proof method, widely used on behavioural relations such as bisimilarity. We study how to develop an analogous theory for inductive behaviour relations, i.e., relations defined from inductive observables. Similarly to the coinductive setting, our theory makes use of (semi)-progressions of the form R->F(R), where R is a relation on processes and F is a function on relations, meaning that there is an appropriate match on the transitions that the processes in R can perform in which the derivatives are in F(R). For a given preorder, an enhancement corresponds to a function sound, i.e., one for which R->F(R) implies that R is contained in the preorder; and similarly for equivalences. We introduce weights on the observables of an inductive relation, and a weight-preserving condition on functions that guarantees soundness. We show that the class of weight-preserving functions contains non-trivial functions and enjoys closure properties with respect to desirable function constructors, so to be able to derive sophisticated sound functions (and hence sophisticated proof techniques) from simpler ones. We consider both strong semantics (in which all actions are treated equally) and weak semantics (in which one abstracts from internal transitions). We test our enhancements on a few non-trivial examples.

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; Inria
DOI Media Attached
10:45
25m
Research 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
25m
Research 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
25m
Research 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