Search

Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA. The automata use an infinite alphabet with a tree structure. We show that the game semantics of any FICA term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation. Moreover, we identify a fragment of FICA that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability., Comment: 18 pages plus appendices

We consider an object calculus in which open terms interact with the environment through interfaces. The calculus is intended to capture the essence of contextual interactions of Middleweight Java code. Using game semantics, we provide fully abstract models for the induced notions of contextual approximation and equivalence. These are the first denotational models of this kind.

This paper presents a method to evaluate untyped lambda terms based on a term tree-traversing technique and judicious use of eta-expansion. The traversal method is inspired by Game Semantics. As traversals explore nodes of the term tree, they dynamically eta-expand some of the subterms to locate their non-immediate arguments. A quantity called dynamic arity determines the necessary amount of eta-expansion to perform at a given point. Traversals are finitely enumerable and characterize the paths in the tree representation of the beta-normal form when it exists. Correctness of the evaluation method follows from the fact that traversals implement leftmost linear reduction, a non-standard reduction strategy based on head linear reduction.

We establish a tight connection between two models of the ��-calculus, namely Milner���s encoding into the ��-calculus (precisely, the Internal ��-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by �� and OGS. We do so for various LTSs: the standard LTS for �� and a new "concurrent" LTS for OGS; an "output-prioritised" LTS for �� and the standard alternating LTS for OGS. We then show that the equivalences induced on ��-terms by all these LTSs (for �� and OGS) coincide. These connections allow us to transfer results and techniques between �� and OGS. In particular we import up-to techniques from �� onto OGS and we derive congruence and compositionality results for OGS from those of ��. The study is illustrated for call-by-value; similar results hold for call-by-name., LIPIcs, Vol. 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), pages 25:1-25:18

International audience; In this paper we provide the first game semantics for the constructive modal logic CK. We first define arenas encoding modal formulas, we then define winning innocent strategies for games on these arenas, and finally we characterize the winning strategies corresponding to proofs in the logic CK. To prove the full-completeness of our semantics, we provide a sequentialization procedure of winning strategies. We conclude the paper by proving their compositionality and showing how our results can be extend to the constructive modal logic CD.

We introduce the concurrent games abstract machine: a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. Our abstract machine takes the shape of a compositional interpretation of terms as Petri structures, certain coloured Petri nets. For the purely functional fragment, our machine is conceptually close to Geometry of Interaction token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. We pair here these ideas with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets. To prove our machine correct, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. We define Petri strategies as those Petri structures obeying the rules of the game. In turn, we show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This not only entails correctness and adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types.

International audience; Using a combination of automata-theoretic and game-semantic techniques, we propose a method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game model. Our first contribution is an automata model over a treestructured infinite data alphabet, called split automata, whose distinctive feature is the separation of control and memory. We show that every FICA term can be translated into such an automaton. Thanks to the structure of split automata, we are able to observe subtle aspects of the underlying game semantics. This enables us to identify a fragment of FICA with iteration and limited synchronisation (but without recursion), for which, in contrast to the whole FICA, a variety of verification problems turn out to be decidable.

Quantum programming languages permit a hardware independent, high-level description of quantum algorithms. In particular, the quantum λ-calculus is a higher-order language with quantum primitives, mixing quantum data and classical control. Giving satisfactory denotational semantics to the quantum λ-calculus is a challenging problem that has attracted significant interest. In the past few years, both static (the quantum relational model) and dynamic (quantum game semantics) denotational models were given, with matching computational adequacy results. However, no model was known to be fully abstract. Our first contribution is a full abstraction result for the games model of the quantum λ-calculus. Full abstraction holds with respect to an observational quotient of strategies, obtained by summing valuations of all states matching a given observable. Our proof method for full abstraction extends a technique recently introduced to prove full abstraction for probabilistic coherence spaces with respect to probabilistic PCF. Our second contribution is an interpretation-preserving functor from quantum games to the quantum relational model, extending a long line of work on connecting static and dynamic denotational models. From this, it follows that the quantum relational model is fully abstract as well. Altogether, this gives a complete denotational landscape for the semantics of the quantum λ-calculus, with static and dynamic models related by a clean functorial correspondence, and both fully abstract.

We are proposing a method for identifying whether the observed behaviour of a function at an interface is consistent with the typical behaviour of a particular programming language. This is a challenging problem with significant potential applications such as in security (intrusion detection) or compiler optimisation (profiling). To represent behaviour we use game semantics, a powerful method of semantic analysis for programming languages. It gives mathematically accurate models (‘fully abstract’) for a wide variety of programming languages. Game-semantic models are combinatorial characterisations of all possible interactions between a term and its syntactic context. Because such interactions can be concretely represented as sets of sequences, it is possible to ask whether they can be learned from examples. Concretely, we are using LSTM, a technique which proved effective in learning natural languages for automatic translation and text synthesis, to learn game-semantic models of sequential and concurrent versions of Idealised Algol (IA), which are algorithmically complex yet can be concisely described. We will measure how accurate the learned models are as a function of the degree of the term and the number of free variables involved. Finally, we will show how to use the learned model to perform latent semantic analysis between concurrent and sequential Idealised Algol.

The present article is a brief informal survey o$\textit {computability logic}$ (CoL). This relatively young and still evolving nonclassical logic can be characterized as a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader sense, being conceived semantically rather than proof-theoretically, CoL is not just a particular theory but an ambitious and challenging long-term project for redeveloping logic. In CoL, logical operators stand for operations on computational problems, formulas represent such problems, and their "truth" is seen as algorithmic solvability. In turn, computational problems – understood in their most general, interactive sense – are defined as games played by a machine against its environment, with "algorithmic solvability" meaning existence of a machine which wins the game against any possible behavior of the environment. With this semantics, CoL provides a systematic answer to the question "What can be computed?", just like classical logic is a systematic tool for telling what is true. Furthermore, as it happens, in positive cases "What can be computed" always allows itself to be replaced by "How can be computed", which makes CoL a problem-solving tool. CoL is a conservative extension of classical first order logic but is otherwise much more expressive than the latter, opening a wide range of new application areas. It relates to intuitionistic and linear logics in a similar fashion, which allows us to say that CoL reconciles and unifies the three traditions of logical thought (and beyond) on the basis of its natural and "universal" game semantics.

Game semantics and session types are two formalisations of the same concept: message-passing open programs following certain protocols. Game semantics represents protocols as games, and programs as strategies; while session types specify protocols, and well-typed π-calculus processes model programs. Giving faithful models of the π-calculus and giving a precise description of strategies as a programming language are two difficult problems. In this paper, we show how these two problems can be tackled at the same time by building an accurate game semantics model of the session π-calculus. Our main contribution is to fill a semantic gap between the synchrony of the (session) π-calculus and the asynchrony of game semantics, by developing an event-structure based game semantics for synchronous concurrent computation. This model supports the first truly concurrent fully abstract (for barbed congruence) interpretation of the synchronous (session) π-calculus. We further strengthen this correspondence, establishing finite definability of asynchronous strategies by the internal session π-calculus. As an application of these results, we propose a faithful encoding of synchronous strategies into asynchronous strategies by call-return protocols, which induces automatically an encoding at the level of processes. Our results bring session types and game semantics into the same picture, proposing the session calculus as a programming language for strategies, and strategies as a very accurate model of the session calculus. We implement a prototype which computes the interpretation of session processes as synchronous strategies.

Quantum programming languages permit a hardware independent, high-level description of quantum algo rithms. In particular, the quantum lambda-calculus is a higher-order programming language with quantum primitives, mixing quantum data and classical control. Giving satisfactory denotational semantics to the quantum lambda-calculus is a challenging problem that has attracted significant interest in the past few years. Several models have been proposed but for those that address the whole quantum λ-calculus, they either do not represent the dynamics of computation, or they lack the compositionality one often expects from denotational models. In this paper, we give the first compositional and interactive model of the full quantum lambda-calculus, based on game semantics. To achieve this we introduce a model of quantum games and strategies, combining quantum data with a representation of the dynamics of computation inspired from causal models of concurrent systems. In this model we first give a computationally adequate interpretation of the affine fragment. Then, we extend the model with a notion of symmetry, allowing us to deal with replication. In this refined setting, we interpret and prove adequacy for the full quantum lambda-calculus. We do this both from a sequential and a parallel interpretation, the latter representing faithfully the causal independence between sub-computations.

International audience; We show how to use operational game semantics as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages: with either general or ground-type references and with either call/cc or no control operator. In game semantics, differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions. The proposed technique, which we call Kripke normal-form bisimulations, combines insights from normal-form bisimulation and Kripke logical relations with game semantics. In particular, the role of the heap and the name history is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, as applicable. The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, it sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.

Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU designs to network protocols have been successfully verified, and there is interest in making them interoperable to tackle end-to-end verification at an even larger scale. Recent work shows that a synthesis of game semantics, refinement-based methods, and abstraction layers has the potential to serve as a common theory of certified components. Integrating certified compilers to such a theory is a critical goal. However, none of the existing variants of CompCert meets the requirements we have identified for this task. CompCertO extends the correctness theorem of CompCert to characterize compiled program components directly in terms of their interaction with each other. Through a careful and compositional treatment of calling conventions, this is achieved with minimal effort.

In his recent and exploratory work on template games and linear logic, Mellies defines sequential and concurrent games as categories with positions as objects and trajectories as morphisms, labelled by a specific synchronization template. In the present paper, we bring the idea one dimension higher and advocate that template games should not be just defined as 1-dimensional categories but as 2-dimensional categories of positions, trajectories and reshufflings (or reschedulings) as 2-cells. In order to achieve the purpose, we take seriously the parallel between asynchrony in concurrency and the Gray tensor product of 2-categories. One technical difficulty on the way is that the category $\mathbb{S} = 2$-Cat of small 2-categories equipped with the Gray tensor product is monoidal, and not cartesian. This prompts us to extend the framework of template games originally formulated by Mellies in a category $\mathbb{S}$ with finite limits, and to upgrade it in the style of Aguiar’s work on quantum groups to the more general situation of a monoidal category $\mathbb{S}$ with coreflexive equalizers, preserved by the tensor product componentwise. We construct in this way an asynchronous template game semantics of multiplicative additive linear logic (MALL) where every formula and every proof is interpreted as a labelled 2-category equipped, respectively, with the structure of Gray comonoid for asynchronous template games, and of Gray bicomodule for asynchronous strategies.

Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to have obtained full abstraction results for programming languages with a variety of computational effects, in a single framework. This is known as the semantic cube or Abramsky's cube, which for sequential deterministic programs establishes a correspondence between certain conditions on strategies (''innocence'', ''well-bracketing'', ''visibility'') and the absence of matching computational effects. Outside of the sequential deterministic realm, there are still a wealth of game semantics-based full abstraction results; but they no longer fit in a unified canvas. In particular, Ghica and Murawski's fully abstract model for shared state concurrency (IA) does not have a matching notion of pure parallel program-we say that parallelism and interference (i.e. state plus semaphores) are entangled. In this paper we construct a causal version of Ghica and Murawski's model, also fully abstract for IA. We provide compositional conditions parallel innocence and sequentiality, respectively banning interference and parallelism, and leading to four full abstraction results. To our knowledge, this is the first extension of Abramsky's semantic cube programme beyond the sequential deterministic world.

Game semantics and winning strategies offer a potential conceptual bridge between semantics and proof systems of logics. We illustrate this link for hybrid logic – an extension of modal logic that allows for explicit reference to worlds within the language. The main result is that the systematic search of winning strategies over all models can be finitized and thus reformulated as a proof system.

Game semantics provides an alternative view on basic logical concepts. Provability games, i.e., games for the validity of a formula provide a link between proof systems and semantics. We present a new type of provability games, namely the Mezhirov game, for minimal propositional logic and two modal systems: the logic of functional frames and the logic of serial frames, i.e., \(\mathbf {KD}\) and prove their adequacy. The games are finite resulting in a finite search for winning strategies.