Layered and object-based game semantics

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.

Complete trace models of state and control

We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either $$\mathrm {call/cc}$$ call / cc or no control operator.Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-order references and $$\mathrm {call/cc}$$ call / cc , constructed in the spirit of operational game semantics. Next we examine the impact of suppressing higher-order references and callcc in contexts and provide an operational explanation for the game-semantic conditions known as visibility and bracketing respectively. This allows us to refine the original model to provide fully abstract trace models of interaction with contexts that need not use higher-order references or $$\mathrm {call/cc}$$ call / cc . Along the way, we discuss the relationship between error- and termination-based contextual testing in each case, and relate the two to trace and complete trace equivalence respectively.Overall, the paper provides a systematic development of operational game semantics for all four cases, which represent the state-based face of the so-called semantic cube.

Leafy automata for higher-order concurrency

Finitary Idealized Concurrent Algol ($$\mathsf {FICA}$$ FICA ) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of $$\mathsf {FICA}$$ FICA , which in principle can be used to prove equivalence and safety of $$\mathsf {FICA}$$ 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 $$\mathsf {FICA}$$ FICA . The automata use an infinite alphabet with a tree structure. We show that the game semantics of any $$\mathsf {FICA}$$ FICA term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a $$\mathsf {FICA}$$ FICA term. Because of the close match with $$\mathsf {FICA}$$ 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 $$\mathsf {FICA}$$ 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.

Bayesian strategies: probabilistic programs as generalised graphical models

We introduceBayesian strategies, a new interpretation of probabilistic programs in game semantics. This interpretation can be seen as a refinement of Bayesian networks.Bayesian strategies are based on a new form ofevent structure, with two causal dependency relations respectively modelling control flow and data flow. This gives a graphical representation for probabilistic programs which resembles the concrete representations used in modern implementations of probabilistic programming.From a theoretical viewpoint, Bayesian strategies provide a rich setting for denotational semantics. To demonstrate this we give a model for a general higher-order programming language with recursion, conditional statements, and primitives for sampling from continuous distributions and trace re-weighting. This is significant because Bayesian networks do not easily support higher-order functions or conditionals.

Dynamic game semantics

The present work achieves a mathematical, in particular syntax-independent, formulation of dynamics and intensionality of computation in terms of games and strategies. Specifically, we give game semantics of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

Computability logic: Giving Caesar what belongs to Caesar

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.