ABSTRACT. FLOC’s policy is that "The open exchange of ideas and the freedom of thought and expression are central to the values and goals of FLoC.  They require an environment that recognizes the inherent worth of every person and group. They flourish in communities that foster mutual understanding and embrace diversity. “  Hardly  controversial  - we are surely more likely to solve the world’s big problems if we draw on as wide a variety of people and talents as we can, and create an environment where they can be their best selves  - but that doesn’t mean that change is easy. I’ll draw on the history of  computing in Oxford and elsewhere to look at  the power of  Intellectual and human diversity, why embracing it is hard, and how we can make progress.

From 1st July 2018 Ursula Martin is a Professor on the School of Informatics of the University of Edinburgh, with affiliations to Oxford’s Mathematical Institute and Wadham College.  She is a Fellow of the Royal Academy of Engineering, and of the Royal Society of Edinburgh. Her research,  initially in algebra,  logic and the use of computers to create mathematical proofs,  now focuses on wider social and cultural approaches to understanding the success and impact of foundational research in computer science and mathematics, and she is the author of a recent book on the mathematics of Ada Lovelace.

ABSTRACT. We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each program location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching, and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.

ABSTRACT. We answer in this paper an open question (known as the "Gamma question"), related to the recent notion of coarse computability, which stems from complexity theory. The question was formulated by Andrews, Cai, Diamondstone, Jockusch and Lempp in "Asymptotic density, computable traceability and 1-randomness" (2016, Fundamenta Mathematicae). The Gamma value of an oracle set measures to what extent each set computable with the oracle is approximable in the sense of density by a computable set. The closer to 1 this value is, the closer the oracle is to being computable. The Gamma question asks whether this value can be strictly in between 0 and 1/2.

In this paper, we pursue some work initiated by Monin and Nies in "A unifying approach to the Gamma question" (2015, LICS). Using notions from computability theory, developed by Monin and Nies, together with some basic techniques from the field of error-correcting codes, we are able to give a negative answer to this question.

The proof we give also provides an answer to a related question, asked by Denis Hirschfeldt in the expository paper "Some questions in computable mathematics" (2017, Computability and Complexity). We also solve the Gamma problem for bases other than 2, answering another question of Monin and Nies.

ABSTRACT. We prove that for every class of graphs $C$ which is nowhere dense, as defined by Nesetril and Ossona de Mendez, and for every first order formula $\phi(\tup x,\tup y)$, whenever one draws a graph $G\in C$ and a subset of its nodes $A$, the number of subsets of $A^{|\tup y|}$ which are of the form $\{\tup v\in A^{|\tup y|} : G\models\phi(\bar u,\tup v)\}$ for some valuation~$\tup u$ of $\tup x$ in $G$ is bounded by $O(|A|^{|\tup x|+\epsilon})$, for every $\epsilon>0$. This provides optimal bounds on the VC-density of first-order definable set systems in nowhere dense graph classes.

We also give two new proofs of upper bounds on quantities in nowhere dense classes which are relevant for their logical treatment. Firstly, we provide a new proof of the fact that nowhere dense classes are uniformly quasi-wide, implying explicit, polynomial upper bounds on the functions relating the two notions. Secondly, we give a new combinatorial proof of a result of Adler and Adler stating that every nowhere dense class of graphs is stable. In contrast to the previous proofs of the above results, our proofs are completely finitistic and constructive, and yield explicit and computable upper bounds on quantities related to uniform quasi-wideness (margins) and stability (ladder indices).

ABSTRACT. In this paper we give a characterization of both Boolean and arithmetic circuit classes of logarithmic depth in the vein of descriptive complexity theory, i.e., the Boolean classes $\textrm{NC}^1$, $\textrm{SAC}^1$ and $\textrm{AC}^1$ as well as their arithmetic counterparts $\#\textrm{NC}^1$, $\#\textrm{SAC}^1$ and $\#\textrm{AC}^1$. We build on Immerman's characterization of constant-depth polynomial-size circuits by formulae of first-order logic, i.e., $\textrm{AC}^0 = \textrm{FO}$, and augment the logical language with an operator for defining relations in an inductive way. Considering slight variations of the new operator, we obtain uniform characterizations of the three just mentioned Boolean classes. The arithmetic classes can then be characterized by functions counting winning strategies in semantic games for formulae characterizing languages in the corresponding Boolean class.

ABSTRACT. For a class K of graphs we consider the following three statements. (i) K has bounded tree-depth. (ii) First-order logic FO has an effective generalized quantifier elimination on K. (iii) The parameterized model checking for FO on K is in para-FO (or equivalently, in para-AC^0). We prove that (i) => (ii) and (ii) <=> (iii). All three statements are equivalent if K is closed under taking subgraphs, but not in general.

By a result due to Elberfeld et al. monadic second-order logic MSO and FO have the same expressive power on every class of graphs of bounded tree-depth. Hence the implication (i) => (iii) holds for MSO, too; it is the analogue of Courcelle's Theorem for tree-depth (instead of tree-width) and para-AC^0 (instead of FPT). In Elberfeld et al. it was already shown that the model-checking for a fixed MSO-property on a class of graphs of bounded tree-depth is in AC^0.

ABSTRACT. It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an al- gebraic characterization by Bojańczyk, et. al., (2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decidability of PDL. We solve this problem in the case k = 2: All languages recognized by forest algebras satisyfing a 2-fold iterated distributive law are in PDL. Furthermore, we show that this class is decidable. This provides a novel nontrivial decidable subclass of PDL, and demonstrates the viability of the proposed approach to deciding PDL in general.

ABSTRACT. We investigate efficient view maintenance for MSO-definable queries over trees or, more precisely, efficient enumeration of answers to MSO-definable queries over trees which are subject to local updates.

We exhibit an algorithm that uses an O(n) preprocessing phase and enumerates answers with O(log(n)) delay between them. When the tree is updated, the algorithm can avoid repeating expensive preprocessing and restart the enumeration phase within O(log(n)) time. This improves over previous results that require O(log^2(n)) time after updates and have O(log^2(n)) delay.

Our algorithms and complexity results in the paper are presented in terms of node-selecting tree automata representing the MSO queries. To present our algorithm, we introduce a balancing scheme for parse trees of forest algebra formulas that is of its own interest.

ABSTRACT. The impredicative $\forall$ operation in Girard's system F permits encodings of various inductive types, such as the natural numbers. However, these types fail to satisfy the relevant $\eta$-rules, and so, in dependent type theory, lack \emph{dependent} elimination rules. We work in Martin-L\"{o}f type theory with an impredicative universe. Using ideas from homotopy type theory, we refine the impredicative encodings so that the dependent elimination rules do hold. We construct a type of natural numbers as an initial algebra, which arises as a subtype of the System F encoding. We also encode some higher inductive types, such as the unit circle $S^1$.

ABSTRACT. Nakano's later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has been difficult to combine these constructs with dependent types in a way that preserves the operational meaning of type theory and admits a simple hierarchy of universes.

We present an operational account of guarded dependent type theory with clocks called Guarded Computational Type Theory, featuring a novel clock intersection connective that enjoys the clock irrelevance principle, as well as a predicative hierarchy of universes which does not require any indexing in clock contexts. Guarded Computational Type Theory is simultaneously a programming language with a rich specification logic, as well as a computational metalanguage that can be used to develop semantics of other languages and logics.

ABSTRACT. While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this article presents an analysis for statically deriving worst-case bounds on the total work performed by message-passing processes. To decompose interacting processes into components that can be analyzed in isolation, the analysis is based on novel resource-aware session types, which describe protocols and resource contracts for inter-process communication. A key innovation is that both messages and processes carry potential to share and amortize cost while communicating. To symbolically express resource usage in a setting without static data structures and intrinsic sizes, resource contracts describe bounds that are functions of interactions between processes. Resource-aware session types combine standard binary session types and type-based amortized resource analysis in a linear type system. This type system is formulated for a core session-type calculus of the language SILL and proved sound with respect to a multiset-based operational cost semantics that tracks the total number of messages that are exchanged in a system. The effectiveness of the analysis is demonstrated by analyzing standard examples from amortized analysis and the literature on session types and by a comparative performance analysis of different concurrent programs implementing the same interface.

ABSTRACT. Reynolds’ original theory of relational parametricity intended to capture the idea that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formalized in a meta-theory with an impredicative universe, such as Martin-Löf Type Theory. A number of more abstract treatments of relational parametricity have since appeared; however, as we show, none of these truly generalize Reynolds’ original theory, in the sense of having it as a direct instance. Indeed, they all require certain strictness conditions that Reynolds’ theory does not satisfy. To correct this, we develop an abstract framework for relational parametricity that does deliver Reynolds’ theory as a direct instance in a natural way. This framework is parametric and uniform with respect to a choice of meta-theory, which allows us to obtain the well-known PER model of Longo and Moggi as a direct instance in a natural way as well. Moreover, we demonstrate on a concrete example that our notion of parametricity also encompasses proof-relevant parametric models, which does not seem to be the case for the well-known definitions. Our framework is thus both descriptive, in that it accounts for well-known models, and prescriptive, in that it identifies properties that good models of relational parametricity should satisfy. It is constructed using the new notion of a split λ2-fibration with isomorphisms, introduced in this paper, which relaxes certain strictness requirements on split λ2-fibrations. Our main theorem is a generalization of Seely’s classical construction of sound models for System F from split λ2-fibrations: we prove that the canonical model of System F induced by every split λ2-fibration with isomorphisms validates System F’s entire equational theory on the nose, independently of the parameterizing meta-theory.

ABSTRACT. We show how the language of Krivine's classical realizability may be used to specify various forms of nondeterminism and relate them with properties of realizability models. More specifically, we introduce an abstract notion of multi-evaluation relation which allows us to finely describe various nondeterministic behaviours. This defines a hierarchy of computational models, ordered by their degree of nondeterminism, similar to Sazonov's degrees of parallelism. What we show is a duality between the structure of the characteristic boolean algebra of a realizability model and the degree of nondeterminism in its underlying computational model.

ABSTRACT. We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic logic along with its modal fragment, and show that the first-order formulas that are non-expansive w.r.t. the natural notion of bisimulation distance are exactly those that can be approximated by modal formulas.

ABSTRACT. We present a sound and complete axiomatization of the Riesz modal logic extended with one inductively defined operator which allows the definition of threshold operators. This logic is capable of interpreting the bounded fragment of the logic probabilistic CTL over discrete and continuous Markov chains.

ABSTRACT. We introduce a logic, called LT, to express properties of transductions, i.e. binary relations from input to output (finite) words. In LT, the input/output dependencies are modelled via an origin function which associates to any position of the output word, the input position from which it originates. LT is well-suited to express relations (which are not necessarily functional), and can express all regular functional transductions, i.e. transductions definable for instance by deterministic two-way transducers. Despite its high expressive power, LT has decidable satisfiability and equivalence problems, with tight non-elementary and elementary complexities, depending on specific representation of LT-formulas. Our main contribution is a synthesis result: from any transduction R defined in LT, it is possible to synthesise a regular functional transduction f such that for all input words u in the domain of R, f is defined and (u,f(u)) is in R. As a consequence, we obtain that any functional transduction is regular iff it is LT-definable. We also investigate the algorithmic and expressiveness properties of several extensions of LT, and explicit a correspondence between transductions and data words. As a side-result, we obtain a new decidable logic for data words.

ABSTRACT. This paper provides an alternate characterization of type-two polynomial-time computability, with the goal of making second-order complexity theory more approachable. We rely on the usual oracle machines to model programs with subroutine calls. In contrast to previous results, the use of higher-order objects as running times is avoided, either explicitly or implicitly. Instead, regular polynomials are used. This is achieved by refining the notion of oracle-polynomial-time introduced by Cook. We impose a further restriction on the oracle interactions to force feasibility. Both the restriction as well as its purpose are very simple: it is well-known that Cook's model allows polynomial depth iteration of functional inputs with no restrictions on size, and thus does not guarantee that polynomial-time computability is preserved. To mend this we restrict the number of lookahead revisions, that is the number of times a query can be asked that is bigger than any of the previous queries. We prove that this leads to a class of feasible functionals and that all feasible problems can be solved within this class if one allows to separate a task into efficiently solvable subtasks. Formally put: the closure of our class under lambda-abstraction and application includes all feasible operations. We also revisit the very similar class of strongly poly-time computable operators previously introduced by Kawamura and Steinberg. We prove it to be strictly included in our class and, somewhat surprisingly, to have the same closure property. This can be attributed to properties of the limited recursion operator: It is not strongly poly-time computable but decomposes into two such operations and lies in our class.

ABSTRACT. We propose LMSO, a proof system inspired from Linear Logic, as a proof-theoretical framework to extract finite-state stream transducers from linear-constructive proofs of omega-regular specifications. We advocate LMSO as a stepping stone toward semi-automatic approaches to Church's synthesis combining computer assisted proofs with automatic decisions procedures. LMSO is correct in the sense that it comes with an automata-based realizability model in which proofs are interpreted as finite-state stream transducers. It is moreover complete, in the sense that every solvable instance of Church's synthesis leads to a linear-constructive proof of the formula specifying the synthesis problem.

ABSTRACT. Differential Linear Logic (DiLL), introduced by Ehrhard and Regnier, extends linear logic with a notion of linear approximation of proofs. While DiLL is a classical logic, classical models of it in which this notion of differentiation corresponds to the usual one of functional analysis were missing. We solve this issue by constructing a model, without higher order, based on nuclear topological vector spaces and distributions with compact support. This interpretation sheds a new light on the rules of DiLL as we are able to understand them as the computational steps for the resolution of Linear Partial Differential Equations. We thus introduce D-DiLL, a deterministic refinement of DiLL with a D-exponential, for which we exhibit a cut-elimination procedure, and a categorical semantics. We recover the rules of DiLL as a special case. For any D Linear Partial Differential operator with constant coefficient, we construct a model of D-DiLL where the D-exponential represent the space of distributions on spaces of functions f such that Dg=f, and where cut-elimination resolves the equation, that is computes g from f.

ABSTRACT. Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard’s extension to MLL1 (first-order MLL) fails to be canonical because of redundant existential witnesses, and present canonical MLL1 proof nets called unification nets without them. For example, while there are infinitely many cut-free Girard nets ∀xPx ⊢ ∃xPx, one per arbitrary choice of witness for ∃x, there is a unique cut-free unification net, with no specified witness.

Redundant existential witnesses cause Girard’s MLL1 nets to suffer from severe complexity issues: (1) cut elimination is non-local and exponential-time (and -space), and (2) some sequents require exponentially large cut-free Girard nets. Unification nets solve both problems: (1) cut elimination is local and linear-time, and (2) a cut-free unification net is only a linear factor larger than its underlying sequent. Since some unification nets are exponentially smaller than corresponding Girard nets and sequent proofs, technical delicacy is required to ensure correctness is polynomial-time (quadratic).

These results extend beyond MLL1 via a broader methodological insight: for canonical quantifiers, the standard parallel/sequential dichotomy of proof nets fails; an implicit/explicit witness dichotomy is also needed. Work in progress extends unification nets to additives and uses them to extend combinatorial proofs [Proofs without syntax, Annals of Mathematics, 2006] to classical first-order logic.

ABSTRACT. We revisit many aspects of the syntactic relations between (variants of) classical linear logic (LL) and (variants of) intuitionistic linear logic (ILL) in the propositional setting.

On the one hand, we study different (parametric) ``negative'' translations from LL to ILL: their expressiveness, the relations with extensions of LL and their use in the proof theory of LL (cut elimination and focusing). In particular, this bridges the intuitionistic restriction on sequents (at most one conclusion) and the focusing property of linear logic. On the other hand, we generalise the known partial results about conservativity of LL over ILL, leading for example to a conservativity proof for LL over tensor logic (TL).

ABSTRACT. We consider distribution-based objectives for Markov Decision Processes (MDP). This class of objectives gives rise to an interesting trade-off between full and partial information. As in full observation, the strategy in the MDP can depend on the state of the system, but similar to partial information, the strategy needs to account for all the states at the same time.

In this paper, we focus on two safety problems that arise naturally in this context, namely, existential and universal safety. Given an MDP A and a closed and convex polytope H of probability distributions over the states of A, the existential safety problem asks whether there exists some distribution ∆ in H and a strategy of A, such that starting from ∆ and repeatedly applying this strategy keeps the distribution forever in H. The universal safety problem asks whether for all distributions in H, there exists such a strategy of A which keeps the distribution forever in H. We prove that both problems are decidable, with tight complexity bounds: we show that existential safety is PTIME-complete, while universal safety is co-NP-complete.

Further, we compare these results with existential and universal safety problems for Rabin’s probabilistic finite-state automata (PFA), the subclass of Partially Observable MDPs which have zero observation. Compared to MDPs, strategies of PFAs are not state dependent. In sharp contrast to the PTIME result, we show that existential safety for PFAs is undecidable. On the other hand, it turns out that the universal safety for PFAs is decidable in EXPTIME, with a co-NP lower bound. Finally, we show that an alternate representation of the input polytope allows us to improve the complexity of universal safety for MDPs and PFAs.

ABSTRACT. The paper deals with finite-state Markov decision processes (MDPs) with integer weights assigned to each state-action pair. New algorithms are presented to classify end components according to their limiting behavior with respect to the accumulated weights. These algorithms are used to provide solutions for two types of fundamental problems for integer-weighted MDPs. First, a polynomial-time algorithm for the classical stochastic shortest path problem is presented, generalizing known results for special classes of weighted MDPs. Second, qualitative probability constraints for weight-bounded (repeated) reachability conditions are addressed. Among others, it is shown that the problem to decide whether a disjunction of weight-bounded reachability conditions holds almost surely under some scheduler belongs to NP ∩ coNP, is solvable in pseudo-polynomial time and is at least as hard as solving two-player mean-payoff games, while the corresponding problem for universal quantification over schedulers is solvable in polynomial time.

ABSTRACT. We present the conditional value-at-risk (CVaR) in the context of Markov chains and Markov decision processes with reachability and mean-payoff objectives. CVaR quantifies risk by means of the expectation of the worst p-quantile. As such it can be used to design risk-averse systems. We consider not only CVaR constraints, but also introduce their conjunction with expectation constraints and quantile constraints (value-at-risk, VaR). We derive lower and upper bounds on the computational complexity of the respective decision problems and characterize the structure of the strategies in terms of memory and randomization.

ABSTRACT. Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies. We set out to unify these models into a basic abstract framework for game semantics, game settings. Our main contribution is the generic construction, for any game setting, of a category of games and strategies. Furthermore, we extend the framework to deal with innocence, and prove that innocent strategies form a subcategory. We finally show that our constructions cover many concrete cases, mainly among the early models and the very recent sheaf-based ones.

ABSTRACT. Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems [C]_S and [C]_L which describe the operational behavior of the Code when confronted to its Environment, both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ ⊢ {P}C{Q} defines a winning and asynchronous strategy [π] with respect to both asynchronous semantics [C]_S and [C]_L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map L : [C]_S → [C]_L from the stateful semantics [C]_S to the stateless semantics [C]_L satisfies a basic fibrational property. We advocate that this fibrational property provide a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.

ABSTRACT. We define a new games model of Probabilistic PCF (PPCF) by enriching thin concurrent games with symmetry, recently introduced by Castellan et al, with probability. This model supports two interpretations of PPCF, one sequential and one parallel. We make the case for this model by exploiting the causal structure of probabilistic concurrent strategies. First, we show that the strategies obtained from PPCF programs have a deadlock-free interaction, and therefore deduce that there is an interpretation-preserving functor from our games to the probabilistic relational model recently proved fully abstract by Ehrhard et al. It follows that our model is intensionally fully abstract. Finally, we propose a definition of probabilistic innocence and prove a finite definability result, leading to a second (independent) proof of full abstraction.

ABSTRACT. Logic and probability are ancient subjects whose unification holds significant potential for the field of artificial intelligence. The BLOG (Bayesian LOGic) language provides a way to write probability models using syntactic and semantic devices from first-order logic. In modern parlance, it is a relational, open-universe probabilistic programming language that allows one to define probability distributions over the entire space of first-order model structures that can be constructed given the constant, function, and predicate symbols of the program. In this public lecture, Stuart Russell will describe the language mainly through examples and cover its application to monitoring the Comprehensive Nuclear-Test-Ban Treaty.