ABSTRACT. The concept of fairness for a concurrent program means that the program must be able to exhibit an unbounded amount of nondeterminism without diverging. Game semantics models of nondeterminism show that this is hard to implement; for example, Harmer and McCusker's model only admits infinite nondeterminism if there is also the possibility of divergence. We solve a long standing problem by giving a fully abstract game semantics for a simple stateful language with a countably infinite nondeterminism primitive. We see that doing so requires us to keep track of infinitary information about strategies, as well as their finite behaviours. The unbounded nondeterminism gives rise to further problems, which can be formalized as a lack of continuity in the language. In order to prove adequacy for our model (which usually requires continuity), we develop a new technique in which we simulate the nondeterminism using a deterministic stateful construction, and then use combinatorial techniques to transfer the result to the nondeterministic language. Lastly, we prove full abstraction for the model; because of the lack of continuity, we cannot deduce this from definability of compact elements in the usual way, and we have to use a stronger universality result instead. We discuss how our techniques could be applied to yield proofs of adequacy for models of nondeterministic PCF, such as those given by Tsukada and Ong.

ABSTRACT. We present a general device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we introduce a novel notion of ‘general signature’ for specifying syntactic constructions. Our signatures subsume classical elementary signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend to much more general examples, as, for instance, commutative n-ary operators, and explicit substitution operators.

In the spirit of Initial Algebra Semantics, we define the 'syntax generated by a signature' to be the initial object - if it exists - in a suitable category. This notion of syntax provides, beyond the desired algebra of terms, a well-behaved substitution and the associated inductive/recursive principles.

Our signatures are ‘general’ in the sense that the existence of syntax is not automatically guaranteed. The main theorem of this work states that a large class of signatures do generate a syntax.

This paper builds upon ideas from a previous attempt by Hirschowitz and Maggesi (FICS 2012), which, in turn, was directly inspired by some earlier work of Ghani-Uustalu and Matthes-Uustalu.

The main theorem presented in the paper is computer-checked within the UniMath system.

ABSTRACT. Combinatorial games are widely used in finite model theory, constraint satisfaction and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraisse games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraisse comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory. .

ABSTRACT. We compare three models of the probabilistic lambda-calculus: the probabilistic Böhm trees of Leventis, the probabilistic concurrent games of Winskel et al., and the probabilistic relational model of Ehrhard et al. Probabilistic Böhm trees and probabilistic strategies are shown to be related by a precise correspondence theorem, in the spirit of existing work for the pure lambda-calculus. Using Leventis' theorem (probabilistic Böhm trees characterise observational equivalence), we derive a full abstraction result for the games model. Then, we relate probabilistic strategies to the weighted relational model, using an interpretation-preserving functor from the former to the latter. We obtain that the relational model is itself fully abstract.

ABSTRACT. Automatic structures are structures that admit a finite presentation via automata. Their most prominent feature is that their theories are decidable. In the literature, one finds automatic structures with non-elementary theory (e.g., the complete binary tree with equal-level predicate) and automatic structures whose theories are at most 3-fold exponential (e.g., Presburger arithmetic or infinite automatic graphs of bounded degree). This observation led Durand-Gasselin to the question whether there are automatic structures of arbitrary high elementary complexity.

We give a positive answer to this question. Namely, we show that for every $h\ge0$ the forest of (infinitely many copies of) all finite trees of height at most $h+2$ is automatic and it's theory is complete for $\STA(\ast, \exp_h(n, \poly(n)), \poly(n))$, an alternating complexity class between $h$-fold exponential time and space. This exact determination of the complexity of the theory of these forests might be of independent interest.

ABSTRACT. Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finite field. The expressive power of FPR properly extends that of FPC and is contained in PTime, but not known to be properly contained. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by [Anderson and Dawar 2017]. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i.e., invariant under all permutations of their inputs). In the case of FPC, the proof of equivalence of circuits and logic rests heavily on the assumption that individual gates compute such symmetric functions and so novel techniques are required to make this work for FPR.

ABSTRACT. Admissible strategies, i.e. those that are not dominated by any other strategy, are a typical rationality notion in game theory. In many classes of games this is justified by results showing that any strategy is admissible or dominated by an admissible strategy. However, in games played on finite graphs with quantitative objectives (as used for reactive synthesis), this is not the case.

We consider increasing chains of strategies instead to recover a satisfactory rationality notion based on dominance in such games. We start with some order-theoretic considerations establishing sufficient criteria for this to work. We then turn our attention to generalized safety/reachability games as a particular application. We propose the notion of maximal uniform chain as the desired dominance-based rationality concept in these games. Decidability of some fundamental questions about uniform chains is established.

ABSTRACT. With the help of an idea of contextual modal logic, we define a logical system \( \lamrefl \) that incorporates monadic reflection, and then investigate delimited continuations through the lens of monadic reflection. Technically, we firstly prove a certain universality of continuation monad, making the character of monadic reflection a little more clear. Next, moving focus to delimited continuations, we present a macro definition of shift/reset by monadic reflection. We then prove that \( \lamreflcont \), a restriction of \( \lamrefl \), has exactly the same provability as \( \lamsrpure \), a system that incorporates shift/reset. Our reconstruction of monadic reflection opens up a path for investigation of delimited continuations with familiar monadic language.

ABSTRACT. The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.

ABSTRACT. Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of verification for reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.