We study contextual interactions in an ML-like language equipped with general references and continuations, focusing on the reachability and approximation problems. Previous work addressed higher-order programs with first-order references in the absence of loops using automata over nested data; however, extending these techniques to programs with loops encountered fundamental technical obstacles, stemming from the need to bound the depth of data. We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops. This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, the first metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing the first full abstraction result for an imperative MetaML-style language. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

Reachability types are a recent approach to modelling sharing in higher-order languages, aiming to provide separation guarantees through typability. The contextual equivalence problem in such a setting is exacerbated by the need to consider reachability-related constraints on the allowable interactions. In particular, they might weaken the ability of contexts to observe sequentiality.In this paper, we investigate contextual equivalence for reach-ability types through the lens of operational game semantics. We provide a sound trace model for a language equipped with reachability types, and show how to refine it to a fully abstract one, which captures a natural notion of equivalence based on allowing terms to share functions and locations consistently with the assigned reachability annotations. We also discuss the corresponding problem of contextual approximation, along with an inequational full abstraction result.This is a first attempt at defining a fully abstract semantics for reachability types.

Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have appeared in the literature: general register assignments; assignments where duplicate register values are disallowed; and assignments without duplicates in which registers cannot be empty. In the general case, we show that the problem is EXPTIME-complete. However, the absence of duplicate values in registers enables us to identify inherent symmetries inside the associated bisimulation relations, which can be used to establish a polynomial bound on the depth of Attacker-winning strategies. Furthermore, they enable a highly succinct representation of the corresponding bisimulations. By exploiting results from group theory and computational group theory, we can then show solvability in PSPACE and NP respectively for the latter two register disciplines. In each case, we find that freshness does not affect the complexity class of the problem. The results allow us to close a complexity gap for language equivalence of deterministic register automata. We show that deterministic language inequivalence for the no-duplicates fragment is NP-complete, which disproves an old conjecture of Sakamoto. Finally, we discover that, unlike in the finite-alphabet case, the addition of pushdown store makes bisimilarity undecidable, even in the case of visibly pushdown storage.

We study the problem of bounding the posterior distribution of discrete probabilistic programs with unbounded support, loops, and conditioning. Loops pose the main difficulty in this setting: even if exact Bayesian inference is possible, the state of the art requires user-provided loop invariant templates. By contrast, we aim to find guaranteed bounds , which sandwich the true distribution. They are fully automated, applicable to more programs and provide more provable guarantees than approximate sampling-based inference. Since lower bounds can be obtained by unrolling loops, the main challenge is upper bounds, and we attack it in two ways. The first is called residual mass semantics , which is a flat bound based on the residual probability mass of a loop. The approach is simple, efficient, and has provable guarantees. The main novelty of our work is the second approach, called geometric bound semantics . It operates on a novel family of distributions, called eventually geometric distributions (EGDs), and can bound the distribution of loops with a new form of loop invariants called contraction invariants . The invariant synthesis problem reduces to a system of polynomial inequality constraints, which is a decidable problem with automated solvers. If a solution exists, it yields an exponentially decreasing bound on the whole distribution, and can therefore bound moments and tail asymptotics as well, not just probabilities as in the first approach. Both semantics enjoy desirable theoretical properties. In particular, we prove soundness and convergence, i.e. the bounds converge to the exact posterior as loops are unrolled further. We also investigate sufficient and necessary conditions for the existence of geometric bounds. On the practical side, we describe Diabolo , a fully-automated implementation of both semantics, and evaluate them on a variety of benchmarks from the literature, demonstrating their general applicability and the utility of the resulting bounds.

We consider contextual equivalence in an ML-like language, where contexts have access to both general references and continuations. We show that in a finitary setting, i.e. when the base types are finite and there is no recursion, the problem is decidable for all programs with first-order references and continuations, assuming they have continuation- and reference-free interfaces. This is the best one can hope for in this case, because the addition of references to functions, to continuations or to references makes the problem undecidable.

We consider a simply-typed call-by-push-value calculus with state, and provide a fully abstract trace model via a labelled transition system (LTS) in the spirit of operational game semantics. By examining the shape of configurations and performing a series of natural optimisation steps based on name recycling, we identify a fragment for which the LTS can be recast as a deterministic visibly pushdown automaton. This implies decidability of contextual equivalence for the fragment identified and solvability in exponential time for terms in canonical form. We also identify a fragment for which these automata are finite-state machines.Further, we use the trace model to prove that translations of prototypical call-by-name (IA) and call-by-value (RML) languages into our call-by-push-value language are fully abstract. This allows our decidability results to be seen as subsuming several results from the literature for IA and RML. We regard our operational approach as a simpler and more intuitive way of deriving such results. The techniques we rely on draw upon simple intuitions from operational semantics and the resultant automata retain operational style, capturing the dynamics of the underlying language.

We present an exact Bayesian inference method for discrete statistical models, which can find exact solutions to a large class of discrete inference problems, even with infinite support and continuous priors. To express such models, we introduce a probabilistic programming language that supports discrete and continuous sampling, discrete observations, affine functions, (stochastic) branching, and conditioning on discrete events. Our key tool is *probability generating functions*: they provide a compact closed-form representation of distributions that are definable by programs, thus enabling the exact computation of posterior probabilities, expectation, variance, and higher moments. Our inference method is provably correct and fully automated in a tool called *Genfer*, which uses automatic differentiation (specifically, Taylor polynomials), but does not require computer algebra. Our experiments show that Genfer is often faster than the existing exact inference tools PSI, Dice, and Prodigy. On a range of real-world inference problems that none of these exact tools can solve, Genfer's performance is competitive with approximate Monte Carlo methods, while avoiding approximation errors.

Probabilistic pushdown automata (recursive state machines) are a widely known model of probabilistic computation associated with many decidable problems concerning termination (time) and linear-time model checking. Higher-order recursion schemes (HORS) are a prominent formalism for the analysis of higher-order computation.

Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second. We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable. Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel's conjecture, when the language is bounded (i.e., a subset of $w_1^*\dots w_m^*$ for some finite words $w_1,\dots,w_m$) or when the automaton has finite ambiguity. On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to $\varepsilon$-differential privacy, for which the optimal constant of the big-O notation is exactly $\exp(\varepsilon)$.

Abstract 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.

Abstract 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.

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

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

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

This article studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely, those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.

Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second. We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable. Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel’s conjecture, when the language is bounded (i.e., a subset of w_1^* … w_m^* for some finite words w_1,… ,w_m). On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to ε-differential privacy, for which the optimal constant of the big-O notation is exactly exp(ε).

Differential privacy is a widely studied notion of privacy for various models of computation, based on measuring differences between probability distributions. We consider (epsilon,delta)-differential privacy in the setting of labelled Markov chains. For a given epsilon, the parameter delta can be captured by a variant of the total variation distance, which we call lv_{alpha} (where alpha = e^{epsilon}). First we study lv_{alpha} directly, showing that it cannot be computed exactly. However, the associated approximation problem turns out to be in PSPACE and #P-hard. Next we introduce a new bisimilarity distance for bounding lv_{alpha} from above, which provides a tighter bound than previously known distances while remaining computable with the same complexity (polynomial time with an NP oracle). We also propose an alternative bound that can be computed in polynomial time. Finally, we illustrate the distances on case studies.

We investigate the expressive power of higher-order recursion schemes (HORS) restricted to linear types. Two formalisms are considered: multiplicative additive HORS (MAHORS), which feature both linear function types and products, and multiplicative HORS (MHORS), based on linear function types only. For MAHORS, we establish an equi-expressivity result with a variant of tree-stack automata. Consequently, we can show that MAHORS are strictly more expressive than first-order HORS, that they are incomparable with second-order HORS, and that the associated branch languages lie at the third level of the collapsible pushdown hierarchy. In the multiplicative case, we show that MHORS are equivalent to a special kind of pushdown automata. It follows that any MHORS can be translated to an equivalent first-order MHORS in polynomial time. Further, we show that MHORS generate regular trees and can be translated to equivalent order-0 HORS in exponential time. Consequently, MHORS turn out to have the same expressive power as 0-HORS but they can be exponentially more concise. Our results are obtained through a combination of techniques from game semantics, the geometry of interaction and automata theory.

We prove that the observational equivalence problem for a finitary fragment of the programming langauge ML is recursively equivalent to the reachability problem for extended branching vector addition systems with states (EBVASS). This result has two natural and independent parts. We first prove that the observational equivalence problem is equivalent to the emptiness problem for a new class of class memory automata equipped with a visibly pushdown stack, called Visibly Pushdown Class Memory Automata (VPCMA). Our proof uses the fully abstract game semantics of the language. We then prove that the VPCMA emptiness problem is equivalent to the reachability problem for EBVASS. The results of this article complete our programme to give an automata classification of the ML types with respect to the observational equivalence problem for closed terms.

Register automata are one of the most studied automata models over infinite alphabets. The complexity of language equivalence for register automata is quite subtle. In general, the problem is undecidable but, in the deterministic case, it is known to be decidable and in NP. Here we propose a polynomial-time algorithm building upon automata- and group-theoretic techniques. The algorithm is applicable to standard register automata with a fixed number of registers as well as their variants with a variable number of registers and ability to generate fresh data values (fresh-register automata). To complement our findings, we also investigate the associated inclusion problem and show that it is PSPACE-complete.

We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is $$\mathsf {unit}\rightarrow \mathsf {unit}\rightarrow \mathsf {unit}$$ . At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation.

Higher-order recursion schemes (HORS) have recently emerged as a promising foundation for higher-order program verification. We examine the impact of enriching HORS with linear types. To that end, we introduce two frameworks that blend non-linear and linear types: a variant of the λY -calculus and an extension of HORS, called linear HORS (LHORS). First we prove that the two formalisms are equivalent and there exist polynomial-time translations between them. Then, in order to support model-checking of (trees generated by) LHORS, we propose a refined version of alternating parity tree automata, called LNAPTA, whose behaviour depends on information about linearity. We show that the complexity of LNAPTA model-checking for LHORS depends on two type-theoretic parameters: linear order and linear depth. The former is in general smaller than the standard notion of order and ignores linear function spaces. In contrast, the latter measures the depth of linear clusters inside a type. Our main result states that LNAPTA model-checking of LHORS of linear order n is n-EXPTIME-complete, when linear depth is fixed. This generalizes and improves upon the classic result of Ong, which relies on the standard notion of order. To illustrate the significance of the result, we consider two applications: the MSO model-checking problem on variants of HORS with case distinction (RSFD and HORSC) on a finite domain and a call-by-value resource verification problem. In both cases, decidability can be established by translation into HORS, but the implied complexity bounds will be suboptimal due to increases in type order. In contrast, we show that the complexity bounds derived by translations into LHORS and appealing to our result are optimal in that they match the respective hardness results.

Linearisability is a central notion for verifying concurrent libraries: a library is proven correct if its operational history can be rearranged into a sequential one that satisfies a given specification. Until now, linearisability has been examined for libraries in which method arguments and method results were of ground type. In this paper we extend linearisability to the general higher-order setting, where methods of arbitrary type can be passed as arguments and returned as values, and establish its soundness.

We investigate reachability in pushdown automata over infinite alphabets. We show that, in terms of reachability/emptiness, these machines can be faithfully represented using only 3r elements of the alphabet, where r is the number of registers. We settle the complexity of associated reachability/emptiness problems. In contrast to register automata, the emptiness problem for pushdown register automata is EXPTIME-complete, independent of the register storage policy used. We also solve the global reachability problem by representing pushdown configurations with a special register automaton. Finally, we examine extensions of pushdown storage to higher orders and show that reachability is undecidable at order 2.

We consider recursion schemes (not assumed to be homogeneously typed , and hence not necessarily safe ) and use them as generators of (possibly infinite) ranked trees. A recursion scheme is essentially a finite typed deterministic term rewriting system that generates, when one applies the rewriting rules ad infinitum , an infinite tree, called its value tree . A fundamental question is to provide an equivalent description of the trees generated by recursion schemes by a class of machines. In this article, we answer this open question by introducing collapsible pushdown automata (CPDA), which are an extension of deterministic (higher-order) pushdown automata. A CPDA generates a tree as follows. One considers its transition graph, unfolds it, and contracts its silent transitions, which leads to an infinite tree, which is finally node labelled thanks to a map from the set of control states of the CPDA to a ranked alphabet. Our contribution is to prove that these two models, higher-order recursion schemes and collapsible pushdown automata, are equi-expressive for generating infinite ranked trees. This is achieved by giving effective transformations in both directions.

Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have appeared in the literature: general register assignments, assignments where duplicate register values are disallowed, and assignments without duplicates in which registers cannot be empty. In the general case, we show that the problem is EXPTIME-complete. However, the absence of duplicate values in registers enables us to identify inherent symmetries inside the associated bisimulation relations, which can be used to establish a polynomial bound on the depth of Attacker-winning strategies. Furthermore, they enable a highly succinct representation of the corresponding bisimulations. By exploiting results from group theory and computational group theory, we can then show solvability in PSPACE and NP respectively for the latter two register disciplines. In each case, we find that freshness does not affect the complexity class of the problem. The results allow us to close a complexity gap for language equivalence of deterministic register automata. We show that deterministic language in equivalence for the no-duplicates fragment is NP-complete, which disproves an old conjecture of Sakamoto. Finally, we discover that, unlike in the finite-alphabet case, the addition of pushdown store makes bisimilarity undecidable, even in the case of visibly pushdown storage.

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.

Higher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, in that respect, are known to be equivalent to a restricted fragment of the lambda-Y-calculus consisting of ground-type terms whose free variables have types of the form o -> ... -> o (with o being a special case). In this paper, we show that any lambda-Y-term (with no restrictions on term type or the types of free variables) can actually be represented by a HORS. More precisely, for any lambda-Y-term M, there exists a HORS generating a tree that faithfully represents M's (eta-long) Böhm tree. In particular, the HORS captures higher-order binding information contained in the Böhm tree. An analogous result holds for finitary PCF. As a consequence, we can reduce a variety of problems related to the lambda-Y-calculus or finitary PCF to problems concerning higher-order recursive schemes. For instance, Böhm tree equivalence can be reduced to the equivalence problem for HORS. Our results also enable MSO model-checking of Böhm trees, despite the general undecidability of the problem.

Given two pushdown automata, the bisimilarity problem asks whether the infinite transition systems they induce are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the best previously known lower bound for this problem. Our lower bound result holds for normed pushdown automata as well.

Abstract Herman’s algorithm is a synchronous randomized protocol for achieving self-stabilization in a token ring consisting of N processes. The interaction of tokens makes the dynamics of the protocol very difficult to analyze. In this paper we study the distribution of the time to stabilization, assuming that there are three tokens in the initial configuration. We show for arbitrary N and for an arbitrary timeout t that the probability of stabilization within time t is minimized by choosing as the initial three-token configuration the configuration in which the tokens are placed equidistantly on the ring. Our result strengthens a corollary of a theorem of McIver and Morgan (Inf. Process Lett. 94(2): 79–84, 2005 ), which states that the expected stabilization time is minimized by the equidistant configuration.

We present a new fully abstract and effectively presentable denotational model for RefML, a paradigmatic higher-order programming language combining call-by-value evaluation and general references in the style of ML. Our model is built using game semantics. In contrast to the previous model by Abramsky, Honda and McCusker, it provides a faithful account of reference types, and the full abstraction result does not rely on the availability of spurious constructs of reference type (bad variables). This is the first denotational model of this kind, preceded only by the trace model recently proposed by Laird.

Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addition to the higher-order push and pop operations, CPDA have an important operation called collapse, whose effect is to "collapse" a stack s to the prefix as indicated by the link from the topmost symbol of s. Our first result is that CPDA are equi-expressive with recursion schemes as generators of (possibly infinite) ranked trees. In one direction, we give a simple algorithm that transforms an order-n CPDA to an order-n recursion scheme that generates the same tree, uniformly for all n Gt= 0. In the other direction, using ideas from game semantics, we give an effective transformation of order-n recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) to order-n CPDA that compute traversals over an abstract syntax graph of the scheme, and hence paths in the tree generated by the scheme. Our equi-expressivity result is the first automata-theoretic characterization of higher-order recursion schemes. Thus CPDA are also a characterization of the simply-typed lambda calculus with recursion (generated from uninterpreted 1st-order symbols) and of (pure) innocent strategies. An important consequence of the equi-expressivity result is that it allows us to reduce decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. Thus we show, as a consequence of a recent result by Ong (modal mu-calculus model-checking of trees generated by recursion schemes is n-EXPTIME complete), that the problem of solving parity games over the configuration graphs of order-n CPDA is n-EXPTIME complete, subsuming several well-known results about the solvability of games over higher-order pushdown graphs by (respectively) Walukiewicz, Cachat, and Knapik et al. Another contribution of our work is a self-contained proof of the same solvability result by generalizing standard techniques in the field. By appealing to our equi-expressivity result, we obtain a new proof of Ong's result. In contrast to higher-order pushdown graphs, we show that the monadic second-order theories of the configuration graphs of CPDA are undecidable. It follows that -- as generators of graphs -- CPDA are strictly more expressive than higher-order pushdown automata.

We investigate the notions of may- and must-approximation in Erratic Idealized Algol (a nondeterministic extension of Idealized Algol), and give explicit characterizations of both using its game model. Notably, must-approximation is captured by a novel preorder on nondeterministic strategies, whose definition is formulated in terms of winning regions in a reachability game. The game is played on traces of one of the strategies and its objective is reaching a complete position without encountering any divergences. The concrete accounts of may- and must-approximation make it possible to derive tight complexity bounds for the corresponding decision problems in the finitary (finite datatypes) variant EIAfof Erratic Idealized Algol. In fact we give a complete classification of the complexity of may- and must-approximation for fragments of EIAfof bounded type order (for terms in beta-normal form). The complexity of the decidable cases ranges from PSPACE to 2-EXPTIME for may-approximation and from EXPSPACE to 3-EXPTIME for must-approximation. Our decidability results rely on a representation theorem for nondeterministic strategies which, for a given term, yields a single (finite or visibly pushdown) automaton capturing both traces and divergences of the corresponding strategy with two distinct sets of final states. The decision procedures producing optimal bounds incorporate numerous automata-theoretic techniques: complementation, determinization, computation of winning regions in reachability games over finite and pushdown graphs as well as product constructions. We see our work as a starting point of research that relates game semantics with other game-based theories.

We consider the following decision problems:ProofNet: Is a given multiplicative linear logic (MLL) proof structure a proof net?EssNet: Is a given essential net (of an intuitionistic MLL sequent) correct?In this article we show how to obtain linear-time algorithms for EssNet. As a corollary, by showing that ProofNet is linear-time reducible to EssNet (by the Trip Translation), we obtain a linear-time algorithm for ProofNet.We show further that it is possible to optimize the verification so that each node of the input structure is visited at most once. Finally, we present linear-time algorithms for sequentializing proof nets and essential nets, that is, for finding derivations of the underlying sequents.

We show how game semantics can be employed to prove that program equivalence in finitary Idealized Algol with active expressions is undecidable. We also investigate a notion of representability of languages by terms and show that finitary Idealized Algol terms of respectively second, third and higher orders define exactly regular, context-free and recursively enumerable languages.

We introduce nominal games for modelling programming languages with dynamically generated local names, as exemplified 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 (or simply FM-sets). We fix an infinite set N of names to be the "atoms" of the FM-theory, and interpret the type v of names as the flat arena whose move-set is N. This approach leads to a clean and precise treatment of fresh names and standard game constructions (such as plays, views, innocent strategies, etc.) that are considered invariant under renaming. The main result is the construction of the first fully-abstract model for the nu-calculus.

Using game semantics we prove that program equivalence is undecidable in finitary Idealized Algol with active expressions as well as in its call-by-value counterpart. It is also shown that strategies corresponding to Idealized Algol terms of respectively second, third and higher orders define exactly regular, context-free and recursively enumerable languages.

We consider the following decision problems. PROOFNET: given a multiplicative linear logic (MLL) proof structure, is it a proof net? ESSNET: given an essential net (of an intuitionistic MLL sequent), is it correct? The authors show that linear-time algorithms for ESSNET can be obtained by constructing the dominator tree of the input essential net. As a corollary, by showing that PROOFNET is linear-time reducible to ESSNET (by the trip translation), we obtain a linear-time algorithm for PROOFNET. We show further that these linear-time algorithms can be optimized to simple one-pass algorithms: each node of the input structure is visited at most once. As another application of dominator trees, we obtain linear time algorithms for sequentializing proof nets (i.e. given a proof net, find a derivation for the underlying MLL sequent) and essential nets.