Game semantics is 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 long short-term memory neural nets (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.

We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.

Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully applied to programming languages. One way is to use abstract machines that pass a token in a fixed graph, along a path indicated by the GoI. These token-passing abstract machines are space efficient, because they handle duplicated computation by repeating the same moves of a token on the fixed graph. Although they can be adapted to obtain sound models with regard to the equational theories of various evaluation strategies for the lambda calculus, it can be at the expense of significant time costs. In this paper we show a token-passing abstract machine that can implement evaluation strategies for the lambda calculus, with certified time efficiency. Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid replicating computation, using the token to find the redexes. The flexibility of interleaving token transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs. This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus by using a strategy of interleaving token passing with as much graph rewriting as possible. Our quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds of possible operations on graphs can be classified as “efficient” following Accattoli’s taxonomy of abstract machines.

This paper proposes a categorical theory of digital circuits based on monoidal categories and graph rewriting. The main goal of this paper is conceptual: to fill a foundational gap in reasoning about digital circuits, which is currently almost exclusively semantic (simulations). The level of abstraction we target is circuits with discrete signal levels, discrete time, and explicit delays, which is appropriate for modelling a range of components such as boolean gates or transistors working in saturation mode. We start with an algebraic signature consisting of the basic electronic components of a given class of circuits and extend it gradually (and in a free way) with further algebraic structure (representing circuit combinations, delays, and feedback), while quotienting it with a notion of equivalence corresponding to input-output observability. Using well-known results about the correspondence between free monoidal categories and graphlike structures we can develop, in a principled way, a graph rewriting system which is shown to be useful in reasoning about such circuits. We illustrate the power of our system by reasoning equationally about a challenging class of circuits: combinational circuits with feedback.

We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. ) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.

Devices with tightly coupled CPUs and FPGA logic allow for the implementation of heterogeneous applications which combine multiple components written in hardware and software languages, including first-party source code and third-party IP. Flexibility in component relationships is important, so that the system designer can move components between software and hardware as the application design evolves. This paper presents a system-level type system and linker, which allows functions in software and hardware components to be directly linked at link time, without requiring any modification or recompilation of the components. The type system is designed to be language agnostic, and exhibits higher-order features, to enables design patterns such as notifications and callbacks to software from within hardware functions. We demonstrate the system through a number of case studies which link compiled software against synthesised hardware in the Xilinx Zynq platform.

This work demonstrates the capabilities of a high-level synthesis tool-chain that allows the compilation of higher order functional programs to gate-level hardware descriptions. Higher order programming allows functions to take functions as parameters. In a hardware context, the latency-insensitive interfaces generated between compiled modules enable late-binding with libraries of pre-existing functions at the place-and-route compilation stage. We demonstrate the completeness and utility of our approach using a case study; a recursive k-means clustering algorithm. The algorithm features complex data-dependent control flow and opportunities to exploit both coarse and fine-grained parallelism.

We present a new abstract machine, called DCESH, which models the execution of higher-order programs running in distributed architectures. DCESH implements a native general remote higher-order function call across node boundaries. It is a modernised version of SECD enriched with specialised communication features required for implementing the remote procedure call mechanism. The key correctness result is that the termination behaviour of the remote procedure call is indistinguishable (bisimilar) to that of a local call. The correctness proofs and the requisite definitions for DCESH and other related abstract machines are formalised using Agda. We also formalise a generic transactional mechanism for transparently handling failure in DCESHs. We use the DCESH as a target architecture for compiling a conventional call-by-value functional language ("Floskel") which can be annotated with node information. Conventional benchmarks show that the single-node performance of Floskel is comparable to that of OCaml, a semantically similar language, and that distribution overheads are not excessive.

We define a new approach to compilation to distributed architectures based on networks of abstract machines. Using it we can implement a generalised and fully transparent form of Remote Procedure Call that supports calling higher-order functions across node boundaries, without sending actual code. Our starting point is the classic Krivine machine, which implements reduction for untyped call-by-name PCF. We successively add the features that we need for distributed execution and show the correctness of each addition. Then we construct a two-level operational semantics, where the high level is a network of communicating machines, and the low level is given by local machine transitions. Using these networks, we arrive at our final system, the \emph{Krivine Net}. We show that Krivine Nets give a correct distributed implementation of the Krivine machine, which preserves both termination and non-termination properties. All the technical results have been formalised and proved correct in \textsc{Agda}. We also implement a prototype compiler which we compare with previous distributing compilers based on Girard's Geometry of Interaction and on Game Semantics.

Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce a bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a (coherent) categorical semantics. This could be a useful type-theoretic and denotational framework for resource-sensitive compilation, and it represents a generalization of several existing type systems. As a nontrivial instance, motivated by hardware compilation, we present a complex new application to calculating and controlling timing of execution in a (recursion-free) higher-order functional programming language with local store.

In this paper we define new abstract machines for game semantics which correspond to networks of conventional computers, and which can be used as an intermediate representation for distributed compilation. This is achieved in two steps. First we introduce the HRAM, a Heap and Register Abstract Machine, an abstraction of a conventional computer, which can be structured into HRAM nets, an abstract point-topoint network model. HRAMs are multi-threaded and subsume communication by tokens (cf. IAM) or jumps (cf. JAM). Game Abstract Machines (GAM), are HRAMs with additional structure at the interface level, but no special operational capabilities. We show that GAMs cannot be naively composed, but composition must be mediated using special HRAM combinators. HRAMs are flexible enough to allow the representation of game models for languages with state (non-innocent games) or concurrency (non-alternating games). We illustrate the potential of this technique by implementing a toy distributed compiler for ICA, a higher-order programming language with shared state concurrency, thus significantly extending our previous distributed PCF compiler. We show that compilation is sound and memory-safe, i.e. no (distributed or local) garbage collection is necessary.

In this paper we construct a new trace model of delay-insensitive asynchronous circuits inspired by Ebergen's model in such a way that it satisfies the compositional properties of a category, with additional monoidal structure and further algebraic properties. These properties taken together lay a solid mathematical foundation for a diagrammatic approach to reasoning about asynchronous circuits, which represents a formalisation of common intuitions about asynchronous circuits and their properties.

In this paper we present a seamless approach to writing and compiling distributed code. By "seamless" we mean that the syntax and semantics of the distributed program remain the same as if it was executed on one node only, except for label annotations indicating on what node sub-terms of the program are to be executed. There are no restrictions on how node labels are to be assigned to sub-terms. We show how the paradigmatic (higher-order functional recursive) programming language PCF, extended with node annotations, can be used for this purpose. The compilation technique is directly inspired by game semantics and the Geometry of Interaction.

Automata representing game-semantic models of programs are meant to operate in environments whose input-output behaviour is constrained by the rules of a game. This can lead to a notion of equivalence between states which is weaker than the conventional notion of bisimulation, since not all actions are available to the environment. An environment which attempts to break the rules of the game is, effectively, mounting a low-level attack against a system. In this paper we show how (and why) to enforce game rules in games-based hardware synthesis and how to use this weaker notion of equivalence, called coherent equivalence, to aggressively minimise automata.

We present a model of games based on nominal sequences, which generalise sequences with atoms and a new notion of coabstraction. This gives a new, precise, and compositional mathematical treatment of justification pointers in game semantics.

Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, by means of rules of a game between the term (the Proponent) and its context (the Opponent). In this game the term is conventionally considered the Proponent and the context the Opponent. In general, the richer the computational features a language has the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence, that is, permission to play any move without combinatorial restrictions. However, we impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves. We introduce a basic C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we show how certain traces explain system-level attacks, i.e.~plausible attacks that are realisable outside of the programming language itself. We also show how allowing {Proponent} to have secrets ensures that some desirable equivalences in the programming language are preserved. Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, as rules of a game between the term and its context. In this game the term is conventionally considered the Proponent and the context the Opponent. In general, the richer the computational features a language has the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence. This Opponent is allowed to play any move, without combinatorial restrictions. However, we will impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves that Opponent cannot play. This is broadly inspired by the Dolev-Yao attacker model of security. For the sake of staying focussed in our presentation we introduce a simple C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we explain how certain inequivalences can be interpreted as system-level attacks, i.e. attacks that are only realizable outside of the programming language itself. We will also show how allowing Proponent to have secrets ensures that some desirable equivalences in the programming language are preserved.

The problem of synthesis of gate-level descriptions of digital circuits from behavioural speci?cations written in higher- level programming languages (hardware compilation) has been studied for a long time yet a definitive solution has not been forthcoming. The emphasis of the first part of this tutorial is methodological, arguing that one of the major obstacles in the way of hardware compilation becoming a useful and mature technology is the lack of a well defined function interface model, i.e. a canonical way in which functions communicate with arguments. In the second part we present a solution based on the Geometry of Synthesis, a semantics-directed approach to hardware compilation.

A synchronous game semantics (one in which several moves may happen simultaneously) is derived from a conventional (sequential) game semantics using a round abstraction algorithm. We choose the programming language Syntactic Control of Interference and McCusker's fully abstract relational model as a convenient starting point and derive a synchronous game model first by refining the relational semantics into a trace semantics, then applying a round abstraction to it. We show that the resulting model is sound but not fully abstract. This work is practically motivated by applications to hardware synthesis via game semantics.

We revisit Alur and Henzinger's "round abstraction" technique as a solution to the problem of implementing a low-latency synchronous process from an asynchronous specification. We use a trace-semantic setting akin to Interaction Categories [Abramsky et. al.], which is also a generalisation of pointer-free game semantic models. We define partial and total correctness for round abstraction relative to composition and we note that in its most general case round abstraction can lead to incorrect behaviour. We identify sufficient properties to guarantee partially correct composition, then we present a framework for round abstraction that is totally correct when applied to asynchronous behaviours. We apply this technique to implementing a hardware compiler from (asynchronous) concurrent programming languages to low-latency synchronous digital circuits via game semantics.

In this paper we extend previous work on the compilation of higher-order imperative languages into digital circuits. We introduce concurrency, an essential feature in the context of hardware compilation, and we use an existing game model to simplify proofs of soundness and adequacy. The synthesised circuits are asynchronous, more precisely they are the "event logic" circuits introduced by Sutherland to implement micropipelines, matching more directly the game model, which is itself asynchronous.

This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs with integer types. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its type system. We use a fully abstract game semantics in the style of Hyland and Ong and a more intensional version of the model that tracks nondeterminism introduced by abstraction in order to detect false counterexamples. These theoretical developments are incorporated in a new model-checking tool, Mage, which implements efficiently the data-abstraction refinement procedure using symbolic and on-the-fly techniques.

After informally reviewing the main concepts from game semantics and placing the development of the field in a historical context we examine its main applications. We focus in particular on finite state model checking, higher order model checking and more recent developments in hardware design.

In this paper we introduce clipping, a new method of syntactic approximation which is motivated by and works in conjunction with a sound and decidable denotational model for a given programming language. Like slicing, clipping reduces the size of the source code in preparation for automatic verification; but unlike slicing it is an imprecise but computationally inexpensive algorithm which does not require a whole-program analysis. The technique of clipping can be framed into an iterated refinement cycle to arbitrarily im prove its precision. We first present this rather simple idea intuitively with some examples, then work out the technical details in the case of an Algol-lik e programming language and a decidable approximation of its game-semantic model inspired by Hankin and Malacaria's lax functor approach. We conclude by prese nting an experimental model checking tool based on these ideas and some toy programs.

We introduce a technique for using conventional predicate abstraction methods to reduce the state-space of models produced using game semantics. We focus on an expressive procedural language that has both local store and local control, a language which enjoys a simple game-semantic model yet is expressive enough to allow non-trivial examples. Our compositional approach allows the verification of incomplete programs (e.g. libraries) and offers the opportunity for new heuristics for improved efficiency. Game-semantic predicate abstraction can be embedded in an abstraction-refinement cycle in a standard way, resulting in an improved version of our experimental model-checking tool Mage, and we illustrate it with several toy examples.

We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with Blast and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.

We introduce a game model for an Algol-like programming language with primitives for parallel composition and synchronization on semaphores. The semantics is based on a simplified version of Hyland-Ong-style games and it emphasizes the intuitive connection between the concurrent nature of games and that of computation. The model is fully abstract for may-equivalence.

We propose a new technique for hardware synthesis from higher-order functional languages with imperative features based on Reynolds Syntactic Control of Interference. The restriction on contraction in the type system is useful for managing the thorny issue of sharing of physical circuits. We use a semantic model inspired by game semantics and the geometry of interaction, and express it directly as a certain class of digital circuits that form a cartesian, monoidal-closed category. A soundness result is given, which is also a correctness result for the compilation technique.

We consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. Having first shown that may-equivalence of second-order open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. To that end we define an annotated type system that controls the number of concurrent threads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. Finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, admits a regular-language representation and thus the restricted observational equivalence is decidable.

This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its syntax. The fully abstract game semantics of the language is used for model-checking safety properties, and an interaction-sequence-based semantics is used for interpreting potentially spurious counterexamples and computing refined abstractions for the next iteration. An implementation based on the FDR model checker demonstrates practicality of the method.

We present a games-based denotational semantics for a quantitative analysis of programming languages. We define a Hyland-Ong-style games framework called slot games, which consists of HO games augmented with a new action called token. We develop a slot-game model for the language Idealized Concurrent Algol by instrumenting the strategies in its HO game model with token actions. We show that the slot-game model is a denotational semantics induced by a notion of observation formalized in the operational theory of improvement of Sands, and we give a full abstraction result. A quantitative analysis of programs has many potential applications, from compiler optimizations to resource-constrained execution and static performance profiling. We illustrate several such applications with putative examples that would be nevertheless difficult, if not impossible, to handle using known operational techniques.

We consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. Having first shown that may-equivalence of second-order open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. To that end we define an annotated type system that controls the number of concurrent threads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. Finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, admits a regular-language representation and thus the restricted observational equivalence is decidable.

We introduce nominal games for modelling programming languages with dynamically generated local names, as examplified by Pitts and Stark's nu-calculus. Inspired by Pitts and Gabbay's recent work on nominal sets, we construct arenas and strategies in the world (or topos) of Fraenkel-Mostowski sets. This approach leads to a clean and precise treatment of fresh names and standard game constructions that are considered invariant under renaming. The main result is the construction of the first fully-abstract model of for the nu-calculus

We describe a software model checking tool founded on game semantics, highlight the underpinning theoretical results and discuss several case studies. The tool is based on an interpretation algorithm defined compositionally on syntax and thus can also handle open programs. Moreover, the models it produces are observationally fully abstract. These features are essential in the modeling and verification of software components such as modules and turn out to lead to very compact models of programs.

We are presenting a semantic analysis of Reynolds's specification logic of Idealized Algol using the parametric operational techniques developed by Pitts. We hope that this more elementary account will make the insights of Tennent and O'Hearn, originally formulated in a functor-category denotational semantics, more accessible to a wider audience. The operational model makes clearer the special nature of term equivalence in the logical setting, identifies some problems in the previous interpretation of negation and also proves the soundness of two new axioms of specification logic. Using the model we show that even a very restricted fragment of specification logic is undecidable.

We introduce a game model for a procedural programming language extended with primitives for parallel composition and synchronization on binary semaphores. The model uses an interleaved version of Hyland-Ong-style games, where most of the original combinatorial constraints on positions are replaced with a simple principle naturally related to static process creation. The model is fully abstract for may-equivalence.

We present a program specification language for Idealized Algol that is compatible both with inferential reasoning and model checking. Model-checking is made possible by the use of an algorithmic, regular-language semantics, which is a representation of the fully-abstract game semantic model of the programming language. Inferential reasoning is carried out using rules based on Hoare's logic of imperative programming, extended to handle procedures and computational side effects. The main logical innovation of this approach is the use of generalized universal quantifiers to specify properties of non-local objects. Together, the regular-language semantics of the programming language and its specification language on the one hand, and the inferential properties of the specification language on the other provide a foundation for compositional software model checking.

We explain how recent developments in game semantics can be applied to reasoning about equivalence of terms in a non-trivial fragment of Idealized Algol (IA) by expressing sets of complete plays as regular languages. Being derived directly from the fully abstract game semantics for IA, our model inherits its good theoretical properties; in fact, for first order IA taken as a stand-alone language the regular language model is fully abstract. The method is algorithmic and formal, which makes it suitable for automation. We show how reasoning is carried out using a meta-language of extended regular expressions, a language for which equivalence is decidable.

Two previous papers of the author show how finitary imperative procedural languages can be modeled using regular languages only, which are representation of fully abstract game models. This paper examines the possibility of using these models as a basis for model-checking Hoare-style partial correctness statements in such languages.

We explain how we can reason about equivalence of terms in a non-trivial fragment of IA by expressing sets of complete plays from the game semantic model as regular languages. The model is fully abstract, concrete and formal , which makes it uniquely suitable for automation. We show how reasoning can be carried out in a meta-language of regular expressions, for which equivalence is decidable.

A survey of the concept of state in programming languages.

A functor-category semantics for pointers.