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

Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus, and algebraic effects to enable the composition of heterogeneous components into larger certified systems. However, in existing models of certified abstraction layers, compositionality is restricted by the lack of encapsulation of state.

In this paper, we present a novel game model for certified abstraction layers where the semantics of layer interfaces and implementations are defined solely based on their observable behaviors. Our key idea is to leverage Reddy’s pioneer work on modeling the semantics of imperative languages not as functions on global states but as objects with their observable behaviors. We show that a layer interface can be modeled as an object type (i.e., a layer signature) plus an object strategy. A layer implementation is then essentially a regular map, in the sense of Reddy, from an object with the underlay signature to that with the overlay signature. A layer implementation is certified when its composition with the underlay object strategy implements the overlay object strategy. We also describe an extension that allows for non-determinism in layer interfaces.

After formulating layer implementations as regular maps between object spaces, we move to concurrency and design a notion of concurrent object space, where sequential traces may be identified modulo permutation of independent operations. We show how to express protected shared object concurrency, and a ticket lock implementation, in a simple model based on regular maps between concurrent object spaces.

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