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.