Search

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.

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.

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.

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.

Formal methods have advanced to the point where the functional correctness of various large system components has been mechanically verified. However, the diversity of semantic models used across projects makes it difficult to connect these component to build larger certified systems. Given this, we seek to embed these models and proofs into a generalpurpose framework where they could interact. We believe that a synthesis of game semantics, the refinement calculus, and algebraic effects can provide such a framework. To combine game semantics and refinement, we replace the downset completion typically used to construct strategies from posets of plays. Using the free completely distributive completion, we construct strategy specifications equipped with arbitrary angelic and demonic choices and ordered by a generalization of alternating refinement. This provides a novel approach to nondeterminism in game semantics. Connecting algebraic effects and game semantics, we interpret effect signatures as games and define two categories of effect signatures and strategy specifications. The resulting models are sufficient to represent the behaviors of a variety of low-level components, including the certified abstraction layers used to verify the operating system kernel CertiKOS.

Many software systems are today built as program families. They permit users to derive a custom program (variant) by selecting suitable configuration options at compile time according to their requirements. Many such program families are safety critical. However, most existing verification techniques are designed to work on the level of single programs. Their application to program families would require to verify each variant in isolation, in a brute force fashion. This approach does not scale in practice due to the (potentially) huge number of possible variants. In this paper, we propose an efficient game semantics based approach for verification of open program families, i.e. program families with undefined components (identifiers). We use symbolic representation of algorithmic game semantics, where symbolic values for inputs are used instead of concrete ones. In this way, we can compactly represent program families with infinite integers as so-called (finite state) featured symbolic automata. Specifically designed model checking algorithms are then employed to uniformly verify safety of all programs (variants) from a family at once using a single compact model and to pinpoint those programs that are unsafe (respectively, safe). We present a prototype tool implementing this approach, and we illustrate its practicality with several examples.

Intensional logic programming is an extension of logic programming based on intensional logic, which includes as special cases both temporal and modal logic programming. In [13] , M. Orgun and W.W. Wadge provided a general framework for capturing the semantics of intensional logic programming languages. They demonstrated that if the intensional operators of a language obey some simple semantic properties, then the programs of the language are guaranteed to have a minimum model semantics. One key property involved in the construction of [13] is the monotonicity of intensional operators. In this paper we consider intensional logic programming from a game-theoretic perspective. In particular we define a two-person game and demonstrate that it can be used in order to define a model for any given intensional program of the class introduced in [13] . Moreover, this model is shown to be identical to the minimum model constructed in [13] . More importantly, we demonstrate that the game is even applicable to intensional languages with non-monotonic operators. In this way we provide the first (to our knowledge) general framework for capturing the semantics of non-monotonic intensional logic programming.

Computational effects which provide access to the flow of control (such as first-class continuations, exceptions and delimited continuations) are important features of higher-order programming languages. There are fundamental differences between them in terms of operational behaviour, expressiveness and implementation, so that understanding how they combine and relate to each other is a challenging objective, with a key role for semantics in making this precise. This paper develops operational and denotational semantics for a hierarchy of programming languages which include combinations of locally declared control prompts to which a program can escape, with first-class continuations which may either capture their enclosing prompts, or be delimited by them. We describe two different hierarchies of models, both based on categories of games and strategies with a computational monad, but obtained using different methodologies. By relaxing combinations of behavioural constraints on strategies with control flow represented by annotation with control pointers we are able to give direct and explicit characterizations of control operators and their effects, including examples characterizing their macro-expressiveness. By constructing a parallel hierarchy of models by applying sequences of monad transformers, and relating these to the direct interpretation of control effects, we obtain games interpretations of higher-level abstractions such as continuations and exceptions, which can be used as the basis for equational reasoning about programs.

We define a new logic programming semantics in terms of abducible atoms. We use it to characterize the stage extensions of an argumentation framework AF by means of an associated normal program PAF. We also define the stage semantics for a special type of normal programs and present a similar characterization.

Game-theoretical interpretation of logical semantics has been first suggested in 1950s. Although it is well know among professionals, it is often excluded from introductory courses in logic. In this paper we examine whether and to what extent would including game semantics in the syllabus of an introductory course of predicate and propositional logic prove to be beneficial to students’ understanding of the subject. To that purpose, we have exposed two groups of undergraduate students of computer science to game semantics as part of recitations for the course Propositional and Predicate Logic. We focus mainly on how this affects students’ mastery of two particular topics – alternating quantification and restricted quantification. Observations were made during the recitations to evaluate any changes in students’ approach to solving relevant problems in classroom. Moreover, before the final test of the recitations one of the groups was given a brief review of game semantics and the other was not. We have measured the difference in performance of these two groups and the results support the hypothesis that game semantics helps students master certain topics of predicate logic. We reference some of the later research in psychology and pedagogy to help us explain this effect.

In this paper, we develop a game-theoretic account of concurrent separation logic. To every execution trace of the Code confronted to the Environment, we associate a specification game where Eve plays for the Code, and Adam for the Environment. The purpose of Eve and Adam is to decompose every intermediate machine state of the execution trace into three pieces: one piece for the Code, one piece for the Environment, and one piece for the available shared resources. We establish the soundness of concurrent separation logic by interpreting every derivation tree of the logic as a winning strategy of this specification game.

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., In Proceedings ICE 2017, arXiv:1711.10708

We develop an extensional semantics for higher-order logic programs with negation, generalizing the technique that was introduced in [Bezem99,Bezem01] for positive higher-order programs. In this way we provide an alternative extensional semantics for higher-order logic programs with negation to the one proposed in [CharalambidisER14]. As an immediate useful consequence of our developments, we define for the language we consider the notions of stratification and local stratification, which generalize the familiar such notions from classical logic programming. We demonstrate that for stratified and locally stratified higher-order logic programs, the proposed semantics never assigns the unknown truth value. We conclude the paper by providing a negative result: we demonstrate that the well-known stable model semantics of classical logic programming, if extended according to the technique of [Bezem99,Bezem01] to higher-order logic programs, does not in general lead to extensional stable models., 24 pages. Submitted to Logical Methods in Computer Science

Any expression M in ULC (the untyped λ-calculus) can be compiled into a rather low-level language we call LLL, whose programs contain none of the traditional implementation devices for functional languages: environments, thunks, closures, etc. A compiled program is first-order functional and has a fixed set of working variables, whose number is independent of M. The generated LLL code in effect traverses the subexpressions of M. We apply the techniques of game semantics to the untyped λ-calculus, but take a more operational viewpoint that uses less mathematical machinery than traditional presentations of game semantics. Further, the untyped lambda calculus ULC is compiled into LLL by partially evaluating a traversal algorithm for ULC.

Godel’s System T is the simply typed lambda calculus extended with numbers and an iterator. The higher-order nature of the language gives it enormous expressive power—the language can represent all the primitive recursive functions and beyond, for instance Ackermann’s function. In this paper we use System T as a minimalistic functional language. We give an interpretation using a data-flow model that incorporates ideas from the geometry of interaction and game semantics. The contribution is a reversible model of higher-order computation which can also serve as a novel compilation technique.

The infinite-valued semantics was introduced in Rondogiannis and Wadge (2005) as a purely logical way for capturing the meaning of well-founded negation in logic programming. The purpose of this paper is threefold: first, to give a non-technical introduction to the infinite-valued semantics; second, to discuss the applicability of the infinite-valued approach to syntactically richer extensions of logic programming; and third, to present the main open problems whose resolution would further enhance the applicability of the technique.

I propose a new semantics for intuitionistic logic, which is a cross between the construction-oriented semantics of Brouwer-Heyting-Kolmogorov and the condition-oriented semantics of Kripke. The new semantics shows how there might be a common semantical underpinning for intuitionistic and classical logic and how intuitionistic logic might thereby be tied to a realist conception of the relationship between language and the world.

We introduce a trace semantics for a call-by-value language with full polymorphism and higher-order references. This is an operational game semantics model based on a nominal interpretation of parametricity whereby polymorphic values are abstracted with special kinds of names. The use of polymorphic references leads to violations of parametricity which we counter by closely recoding the disclosure of typing information in the semantics. We prove the model sound for the full language and strengthen our result to full abstraction for a large fragment where polymorphic references obey specific inhabitation conditions.

This work proposes a declarative semantics based on a fuzzy variant of the classical notion of least Herbrand model for the so-called FASILL language (acronym of “Fuzzy Aggregators and Similarity Into a Logic Language”) which has been recently designed and implemented in our research group for coping with implicit/explicit truth degree annotations, a great variety of connectives and unification by similarity.

We describe a denotational, intensional semantics for programs with polymorphic types with bounded quantification, in which phenomena such as inheritance between stateful objects may be represented and studied. Our model is developed from a game semantics for unbounded polymorphism, by establishing dinaturality properties of generic strategies, and using them to give a new construction for interpreting subtyping constraints and bounded quantification. We use this construction to give a denotational semantics for a programming language with general references and an expressive polymorphic typing system. We show that full abstraction fails in general in this model, but that it holds for all terms at a rich collection of bounded types.

Logic rules and inference are fundamental in computer science and have been studied extensively. However, prior semantics of logic languages can have subtle implications and can disagree significantly, on even very simple programs, including in attempting to solve the well-known Russell’s paradox. These semantics are often non-intuitive and hard-to-understand when unrestricted negation is used in recursion. This paper describes a simple new semantics for logic rules, founded semantics, and its straightforward extension to another simple new semantics, constraint semantics, that unify the core of different prior semantics. The new semantics support unrestricted negation, as well as unrestricted existential and universal quantifications. They are uniquely expressive and intuitive by allowing assumptions about the predicates, rules and reasoning to be specified explicitly, as simple and precise binary choices. They are completely declarative and relate cleanly to prior semantics. In addition, founded semantics can be computed in linear time in the size of the ground program.

Higher-order model checking - the model checking of trees generated by higher-order recursion schemes (HORS) - is a natural generalisation of finite-state and pushdown model checking. Recent work has shown that it can serve as a basis for software model checking for functional languages such as ML and Haskell. In this paper, we introduce higher-order recursion schemes with cases (HORSC), which extend HORS with a definition-by-cases construct (to express program branching based on data) and non-determinism (to express abstractions of behaviours). This paper is a study of the universal HORSC model checking problem for deterministic trivial automata : does the automaton accept every tree in the tree language generated by the given HORSC? We first characterise the model checking problem by an intersection type system extended with a carefully restricted form of union types. We then present an algorithm for deciding the model checking problem, which is based on the notion of traversals induced by the fully abstract game semantics of these schemes, but presented as a goal-directed construction of derivations in the intersection and union type system. We view HORSC model checking as a suitable backend engine for an approach to verifying functional programs. We have implemented the algorithm in a tool called TravMC , and demonstrated its effectiveness on a test suite of programs, including abstract models of functional programs obtained via an abstraction-refinement procedure from pattern-matching recursion schemes.

Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages—languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the “semantic cube”: fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences.In this paper, we marry the aspirations of the semantic cube to the powerful proof method of step-indexed Kripke logical relations. Building on recent work of Ahmed et al. (2009), we define the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power of our language—namely, the restriction to first-order state and/or the removal of call/cc—we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of state transition systems to model the way in which properties of local state evolve over time.

We examine different approaches to reasoning about program equivalence in a higher-order language which incorporates a basic notion of state: references of unit type (names). In particular, we present three such methods stemming from logical relations, bisimulation techniques and game semantics respectively. The methods are tested against a surprisingly difficult example equivalence at second order which exploits the intricacies of the language with respect to privacy and flow of names, and the ensuing notion of local state.

We present the RFuzzy framework, a Prolog-based tool for representing and reasoning with fuzzy information. The advantages of our framework in comparison to previous tools along this line of research are its easy, user-friendly syntax, and its expressivity through the availability of default values and types. In this approach we describe the formal syntax, the operational semantics and the declarative semantics of RFuzzy (based on a lattice). A least model semantics, a least fixpoint semantics and an operational semantics are introduced and their equivalence is proven. We provide a real implementation that is free and available. (It can be downloaded from http://babel.ls.fi.upm.es/software/rfuzzy/.) Besides implementation details, we also discuss some actual applications using RFuzzy.

This paper presents a game semantics for a simply-typed λ-calculus with qbits constants and associated quantum operations. The resulting language is expressive enough to encode any quantum circuit. The language uses a notion of extended variable, similar to that seen in functional languages with pattern matching, but adapted to the needs of dealing with tensor products. The game semantics is constructed from classical game semantics using quantum interventions as questions and measurements results as answers. A soundness result for the semantics is given.

In the literature, there are several approaches which try to perform common sense reasoning. Among them, the approaches which have probably received the most attention the last two decades are the approaches based on logic programming semantics with negation as failure and argumentation theory. Even though both approaches have their own features, it seems that they share some common behaviours which can be studied by considering the close relationship between logic programming semantics and extension-based argumentation semantics. In this paper, we will present a general recursive schema for defining new logic programming semantics. This schema takes as input any basic logic programming semantics, such as the stable model semantics, and gives as output a new logic programming semantics which satisfies some desired properties such as relevance and the existence of the intended models for every normal program. We will see that these new logic programming semantics can define candidate extension-based argumentation semantics. These new argumentation semantics will overcome some of the weakness of the extension-based argumentation semantics based on admissible sets. In fact, we will see that some of these new argumentation semantics have similar behaviour to the extension-based argumentation semantics built in terms of strongly connected components.

Game Semantics has successfully provided fully abstract models for a variety of programming languages not possible using other denotational approaches. Although it is a flexible and accurate way to give semantics to a language, its underlying mathematics is awkward. For example, the proofs that strategies compose associatively and maintain properties imposed on them such as innocence are intricate and require a lot of attention. This work aims at beginning to provide a more elegant and uniform mathematical ground for Game Semantics. Our quest is to find mathematical entities that will retain the properties that make games an accurate way to give semantics to programs, yet that are simple and familiar to work with. Our main result is a full, faithful strong monoidal embedding of a category of games into a category of coherence spaces, where composition is simple composition of relations.

Using game semantics, we prove a full abstraction result (with respect to the may-testing preorder) for Idealized Algol augmented with parallel composition (IA||). Although it is common knowledge that semaphores can be implemented using shared memory, we find that semaphores do not extend IA|| conservatively. We explain the reasons for the mismatch.

This paper extends previous work on the compilation of higher-order imperative languages into digital circuits [Ghica, D.R., Geometry of Synthesis: a structured approach to VLSI design, in: POPL, 2007, pp. 363–375.]. We introduce concurrency, an essential feature in the context of hardware compilation and we re-use an existing game model to simplify correctness proofs. The target designs we compile to are asynchronous event-logic circuits, which naturally match the asynchronous game model of the language.

We model security protocols as games using concepts of game semantics. Using this model we ascribe semantics to protocols written in the standard simple arrow notation. According to the semantics, a protocol is interpreted as a set of strategies over a game tree that represents the type of the protocol. The model uses abstract computation functions and message frames in order to model internal computations and knowledge of agents and the intruder. Moreover, in order to specify properties of the model, a logic that deals with games and strategies is developed. A tableau-based proof system is given for the logic, which can serve as a basis for a model checking algorithm. This approach allows us to model a wide range of security protocol types and verify different properties instead of using a variety of methods as is currently the practice. Furthermore, the analyzed protocols are specified using only the simple arrow notation heavily used by protocol designers and by practitioners.

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.

The paper provides an overview of the s-semantic approach to the semantics of logic programs which had been developed about twenty years ago. The aim of such an approach was that of providing a suitable base for program analysis by means of a semantics which really captures the operational behavior of logic programs, and thus offers useful notions of observable program equivalences. The semantics is given in terms of extended interpretations, which are more expressive than Herbrand interpretations, extends the standard Herbrand semantics, and can be obtained as a result of both top-down and bottom-up constructions. The approach has been applied to several extensions of positive logic programs and used to develop semantic-based techniques for program analysis, verification and transformation.

We consider a simple and well-known category of alternating games (also known as sequential data structures) and several categories derived from it. In each case, we present an extension of Plotkin's language FPC (or a suitable linearization thereof) which defines all computable strategies of appropriate types. The quest for such languages results in a novel selection of language primitives for state encapsulation, coroutining and backtracking.

International audience; We study the algebraic structure of a programming language with higher-order store, in the style of ML references. Instead of working directly on the operational semantics of the language, we consider its fully abstract game semantics defined by Abramsky, Honda and McCusker one decade ago. This alternative description of the language is nice and conceptual, except on one significant point: the interactive behavior of the higher-order memory cell is reflected in the model by a strategy $\mathtt{cell}$ whose definition remains slightly enigmatic. The purpose of our work is precisely to clarify this point, by providing a neat algebraic definition of the strategy. This conceptual reconstruction of the memory cell is based on the idea that a general reference behaves essentially as a linear feedback (or trace operator) in an ambient category of Conway games and strategies. This analysis leads to a purely axiomatic proof of soundness of the model, based on a natural refinement of the replication modality of tensor logic.

Reynolds' view of a storage cell as an expression-acceptor pair has been widely used by researchers. We present a different way of organizing semantics of state, and in particular game semantics, by adding to typing contexts a zone for global state. This has the following advantages. Firstly, it causes the “good variable” equations for references to be validated, and also the noninterference equations between distinct references, as enumerated by Plotkin and Power. Secondly, it gives a cleaner categorical structure based on the configurations (state + program) used to describe operational semantics. Thirdly, it leads to a simpler proof that the game semantics is sound and adequate with respect to the operational semantics.

We describe a fully abstract semantics for a simple functional language with locally declared names which may be used as pointers to names. It is based on a category of dialogue games acted upon by the group of natural number automorphisms. This allows a formal, semantic characterization of the key properties of names such as freshness and locality. We describe a model of the call-by-value λ -calculus (a closed Freyd category) based on these games, and show that it can be used to interpret the nu-calculus of Pitts and Stark. We then construct a model of our pointer-language by extending our category of games with an explicit representation of the store, using a notion of semantic garbage-collection to erase inaccessible pointers. Using factorization and decomposition techniques, we show that the compact elements of our model are definable as terms, and hence it is fully abstract.

We present an infinite-game characterization of the well-founded semantics for function-free logic programs with negation. Our game is a simple generalization of the standard game for negation-less logic programs introduced by van Emden [M.H. van Emden, Quantitative deduction and its fixpoint theory, Journal of Logic Programming 3 (1) (1986) 37–53] in which two players, the Believer and the Doubter , compete by trying to prove (respectively disprove) a query. The standard game is equivalent to the minimum Herbrand model semantics of logic programming in the sense that a query succeeds in the minimum model semantics iff the Believer has a winning strategy for the game which begins with the Doubter doubting this query. The game for programs with negation that we propose follows the same rules as the standard one, except that the players swap roles every time the play “passes through” negation. We start our investigation by establishing the determinacy of the new game by using some classical tools from the theory of infinite-games. Our determinacy result immediately provides a novel and purely game-theoretic characterization of the semantics of negation in logic programming. We proceed to establish the connections of the game semantics to the existing semantic approaches for logic programming with negation. For this purpose, we first define a refined version of the game that uses degrees of winning and losing for the two players. We then demonstrate that this refined game corresponds exactly to the infinite-valued minimum model semantics of negation [P. Rondogiannis,W.W. Wadge, Minimum model semantics for logic programs with negation-as-failure, ACM Transactions on Computational Logic 6 (2) (2005) 441–467]. This immediately implies that the unrefined game is equivalent to the well-founded semantics (since the infinite-valued semantics is a refinement of the well-founded semantics).

We solve a longstanding problem by providing a denotational model for nondeterministic programs that identifies two programs iff they have the same range of possible behaviours. We discuss the difficulties with traditional approaches, where divergence is bottom or where a term denotes a function from a set of environments. We see that making forcing explicit, in the manner of game semantics, allows us to avoid these problems. We begin by modelling a first-order language with sequential I/O and unbounded nondeterminism (no harder to model, using this method, than finite nondeterminism). Then we extend the model to a calculus with higher-order and recursive types, by adapting standard game semantics. Traditional adequacy proofs using logical relations are not applicable, so we use instead a novel hiding and unhiding argument.

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.

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.

20 pages; International audience; In this paper I present a game model for the semantical analysis of handshake circuits. I show how the model captures effectively the composition of circuits in an associative way. Then I build a compact-closed category of handshake games and handshake strategies. I then consider the language Tangram and I define a semantics for this language simply by giving a denotation in the model to each handshake component that is used in the compilation of Tangram programs.