ABSTRACT. We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of n-element structures that can be distinguished by a k-variable first-order sentence but where every such sentence has quantifier depth at least n^{k/log(k)}. Our trade-offs also apply to first-order counting logic, and by the known connection to the k-dimensional Weisfeiler-Leman algorithm imply near-optimal lower bounds on the number of refinement iterations. A key component in our proofs is the hardness condensation technique recently introduced by [Razborov '15].

ABSTRACT. We study the existence of Hanf normal forms for extensions FO(Q) of first-order logic by sets Q of unary counting quantifiers (i.e., subsets of the natural numbers). A formula is in Hanf normal form if it is a Boolean combination of statements of the form "the number of witnesses y of psi(x, y) belongs to Q" where Q is a unary counting quantifier and psi describes the isomorphism type of a local neighbourhood around its free variables x,y.

We show that a formula from FO(Q) can be transformed into a formula in Hanf normal form that is equivalent on all structures of degree =< d if, and only if, all counting quantifiers occuring in the formula are ultimately periodic. This transformation can be carried out in worst-case optimal 3-fold exponential time.

In particular, this yields an algorithmic version of Nurmonen's extension of Hanf's theorem for first-order logic with modulo counting quantifiers.

ABSTRACT. We show that on graphs with n vertices the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n^2/log(n)) iterations to reach stabilization. This in particular shows that the previously best, trivial upper bound of O(n^2) is asymptotically not tight. In the logic setting this translates to the statement that if two graphs of size n can be distinguished by a formula in first order logic with counting with 3 variables (i.e., in C3) then they can also be distinguished by a C3-formula that has quantifier depth at most O(n^2/log(n)).

To prove the result we define a game between two players that enables us to decouple the causal dependencies between the processes happening simultaneously over several iterations of the algorithm. This allows us to treat large color classes and small color classes separately. As part of our proof we show that for graphs with bounded color classes, the number of iterations is at most linear in the number of vertices. This also yields a corresponding statement in first order logic with counting.

Similar results can be obtained in the absence of counting, i.e., for the logic L3.

ABSTRACT. We provide a wide-ranging study of the scenario where a subset of the relations in a schema are visible --- that is, their complete contents are known --- while the remaining relations are invisible. The schema has integrity constraints which may relate the visible relations to the invisible ones. We want to determine which information about a query (a positive existential sentence) can be inferred from the visible instance and the constraints. We consider both positive and negative query information, that is, whether the query or its negation holds. We consider the instance-level version of the problem, where both the query and the visible instance are given, as well as the schema-level version, where we want to know whether truth or falsity of the query can be inferred in some instance of the schema.

ABSTRACT. We revisit coinductive proof principles from a lattice theoretic point of view.

By associating to any monotone function a function which we call the companion, we give a new presentation of both Knaster-Tarski's seminal result, and of the more recent theory of enhancements of the coinductive proof method (up-to techniques).

The resulting theory encompasses parametrised coinduction, as recently proposed by Hur et al., and second-order reasoning, i.e., the ability to reason coinductively about the enhancements themselves. It moreover resolves an historical peculiarity about up-to context techniques.

Based on these results, we present an open-ended proof system allowing one to perform proofs on-the-fly and to neatly separate inductive and coinductive phases.

ABSTRACT. Guarded recursion is a form of recursion where recursive calls are guarded by delay modalities. Previous work has shown how guarded recursion is useful for reasoning operationally about programming languages with advanced features including general references, recursive types, countable non-determinism and concurrency.

Guarded recursion also offers a way of adding recursion to type theory while maintaining logical consistency. In previous work we initiated a programme of denotational semantics in type theory using guarded recursion, by constructing a computationally adequate model of the language PCF (simply typed lambda calculus with fixed points). This model was intensional in that it could distinguish between computations computing the same result using a different number of fixed point unfoldings.

In this work we show how also programming languages with recursive types can be given denotational semantics in type theory with guarded recursion. More precisely, we give a computationally adequate denotational semantics to the language FPC (simply typed lambda calculus extended with recursive types), modelling recursive types using guarded recursive types. The model is intensional in the same way as was the case in previous work, but we show how to recover extensionality using a logical relation.

All constructions and reasoning in this paper, including proofs of theorems such as soundness and adequacy, are by (informal) reasoning in type theory, often using guarded recursion.

ABSTRACT. We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For example, all well-known basic types and type formers that are needed for using this type theory as a logic are definable: propositional connectives, like falsity, conjunction, disjunction, and function space, dependent function space, existential quantification, equality, natural numbers, vectors etc. The reduction relation on terms consists solely of a rule for recursion and a rule for corecursion. The reduction relations for well-known types arise from that. To further support the introduction of this new type theory, we also prove fundamental properties of its term calculus. Most importantly, we prove subject reduction and strong normalisation of the reduction relation, which gives computational meaning to the terms.

ABSTRACT. We describe computational models, notably Turing and counter machines, as state transition systems with side effects. Side effects are expressed via an algebraic signature and interpreted over comodels for that signature; basically, comodels describe the memory model while the transition system captures the control structure. Completeness of equational reasoning over comodels is known to be a subtle issue. We identify a criterion on equational theories and classes of comodels that guarantees completeness, over the given class of comodels, of the standard equational calculus, and show that this criterion is satisfied in our leading examples. Based on such a complete equational axiomatization of the memory model, we then give a complete inductive-coinductive calculus for program equivalence in the full computational model. This calculus is phrased in terms of simulation between states, where a state simulates another if it has at least the same terminating computations, with the same cumulative effect on global state.

ABSTRACT. We describe an interpretation of recursive computation in a symmetric monoidal category with infinite biproducts and cofree commutative comonoids (for instance, the category of free modules over a complete semiring). Such categories play a significant role in ``quantitative'' models of computation: they bear a canonical complete monoid enrichment, but may not be cpo-enriched, making standard techniques for reasoning about fixed points unavailable. By constructing a bifree algebra for the cofree exponential, we obtain fixed points for morphisms in its co-Kleisli category without requiring any order-theoretic structure. These fixed points corresponding to infinite sums of finitary approximants indexed over the nested finite multisets, each representing a unique call-pattern for computation of the fixed point. We illustrate this construction by using it to give a denotational semantics for PCF with non-deterministic choice and scalar weights from a complete semiring, proving that this is computationally adequate with respect to an operational semantics which evaluates a term by taking a weighted sum of the residues of its terminating reduction paths.

ABSTRACT. Hella et al. (PODC 2012, Distributed Computing 2015) identified seven different message-passing models of distributed computing---one of which is the port-numbering model---and provided a complete classification of their computational power relative to each other. However, their method for simulating the ability to count incoming messages causes an additive overhead of $2\Delta-2$ communication rounds, and it was not clear, if this is actually optimal. In this paper we give a positive answer, by using bisimulation as our main tool: there is a matching linear-in-$\Delta$ lower bound. This closes the final gap in our understanding of the models, with respect to the number of communication rounds. By a previously identified connection to modal logic, our result has also implications to the relationship between multimodal logic and graded multimodal logic.

ABSTRACT. This paper studies forcing translations of proofs in dependent type theory, through the Curry-Howard correspondence. Based on a call-by-push-value decomposition, we synthesize two simply-typed translations:

i) one call-by-value, corresponding to the translation derived from the presheaf construction as studied in a previous paper;

ii) one call-by-name, whose intuitions already appear in Krivine and Miquel's work.

Focusing on the call-by-name translation, we adapt it to the dependent case and prove that it is compatible with the definitional equality of our system, thus avoiding coherence problems. This allows us to use any category as forcing conditions, which is out of reach with the call-by-value translation. Our construction also exploits the notion of storage operators in order to interpret dependent elimination for inductive types. This is a novel example of a dependent theory with side-effects, clarifiying how dependent elimination for inductive types must be restricted in a non-pure setting.

Being implemented as a Coq plugin, this work gives the possibility to formalize easily consistency results, for instance the consistency of the negation of Voevodsky's univalence axiom.

ABSTRACT. Modal mu-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-theoretical side. Nevertheless, axiomatizations have been given for both linear and branching time mu-calculi, with quite involved completeness arguments. We come back to this central problem, considering it from a proof search viewpoint, and provide some new completeness arguments in the linear time mu-calculus. Our results only deal with restricted classes of formulas that closely correspond to (non-alternating) omega-automata but, compared to earlier proofs, our completeness arguments are direct and constructive. We first consider a natural circular proof system based on sequent calculus, and show that it is complete for inclusions of parity automata directly expressed as formulas, making use of Safra's construction directly in proof search. We then consider the corresponding finitary proof system, featuring (co)induction rules, and provide a partial translation result from circular to finitary proofs. This yields completeness of the finitary proof system for inclusions of sufficiently deterministic parity automata, and finally for arbitrary Büchi automata.

ABSTRACT. The algebraic theory of rational languages has provided powerful decidability results. Among them, one of the most fundamental is the definability of a rational language in the class of aperiodic languages, i.e. languages recognized by finite automata whose transition relation defines an aperiodic congruence. An important corollary of this result is the first-order definability of monadic second-order formulas over finite words. Our goal is to extend these results to rational transductions, i.e. word functions realized by finite transducers. We take an algebraic approach and consider definability problems of rational transductions in a given variety of congruences (or monoids). The strength of the algebraic theory of rational languages relies on the existence of a congruence canonically attached to every language, the syntactic congruence. In a similar spirit, Reutenauer and Schützenberger have defined a canonical device for rational transductions, that we extend to establish our main contribution: an effective characterization of V-transductions, i.e. rational transductions realizable by transducers whose transition relation defines a congruence in a (decidable) variety V. In particular, it provides an algorithm to decide the definability of a rational transduction by an aperiodic finite transducer. Using those results, we show that the FO-definability of a rational transduction is decidable, where FO-definable means definable in a first-order restriction of logical transducers à la Courcelle.

ABSTRACT. Order-invariant formulas access an ordering on a structure's universe, but the model relation is independent of the used ordering. Order invariance is frequently used for logic-based approaches in computer science. Order-invariant formulas capture unordered problems of complexity classes and they model the independence of the answer to a database query from low-level aspects of databases. We study the expressive power of order-invariant monadic second-order (MSO) and first-order (FO) logic on restricted classes of structures that admit certain forms of tree decompositions (not necessarily of bounded width).

While order-invariant MSO is more expressive than MSO and, even, CMSO (MSO with modulo-counting predicates), we show that order-invariant MSO and CMSO are equally expressive on graphs of bounded tree width and on planar graphs. This extends an earlier result for trees due to Courcelle. Moreover, we show that all properties definable in order-invariant FO are also definable in MSO on these classes. These results are applications of a theorem that shows how to lift up definability results for order-invariant logics from the bags of a graph's tree decomposition to the graph itself.

ABSTRACT. We prove a conjecture of Courcelle which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the following sense: constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. While the forward implication is a classic fact known as Courcelle's theorem, the converse direction remained open.

ABSTRACT. In model theory, a model companion of a theory is a first-order description of the models where all solvable systems of equations and non-equations have solutions. We newly apply this model-theoretic framework in the realm of monadic second-order and temporal logic: we show that bisimulation-invariant MSO on trees gives the model companion for "fair CTL", the enrichment of CTL with fairness constraints. To achieve this, we give a completeness proof for the logic fair CTL which combines tableaux and Stone duality, and a fair CTL encoding of the automata for the modal μ-calculus. Moreover, we also show that MSO on binary trees is the model companion of binary deterministic fair CTL.

ABSTRACT. Interaction graphs were introduced as a general, uniform, construction of dynamic models of linear logic, encompassing all Geometry of Interaction (GoI) constructions introduced so far. This series of work was inspired from Girard’s hyperfinite GoI, and develops a quantitative approach that should be understood as a dynamic version of weighted relational models. Until now, the interaction graphs framework has been shown to deal with exponentials for the constrained system ELL (Elementary Linear Logic) while keeping its quantitative aspect. An adaptation of older constructions by Girard can be used to define “full” exponentials, but at the cost of these quantitative features. We show here that allowing interpretations of proofs to use continuous (yet finite in a measure-theoretic sense) sets of states, as opposed to earlier constructions in which these sets of states were discrete (and finite), provides quantitative models for full linear logic with second order quantification.

ABSTRACT. Proof nets for MLL (unit-free multiplicative linear logic) and ALL (unit-free additive linear logic) are graphical abstractions of proofs which are efficient (proofs translate in linear time) and canonical (invariant under rule commutation). This paper solves a three-decade open problem: are there efficient canonical proof nets for MALL (unit-free multiplicative-additive linear logic)?

Honouring MLL and ALL canonicity, in which all commutations are strictly local proof-tree rewrites, we define local canonicity for MALL: invariance under local rule commutation. We present new proof nets for MALL, called conflict nets, which are both efficient and locally canonical.

ABSTRACT. We introduce a linear infinitary lambda-calculus in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the infinitary applicative lambda-calculus and is universal for computations over infinite strings. What is particularly interesting about the calculus is that the refinement induced by linear logic allows to restrict both modalities so as to get calculi which are terminating inductively and productive coinductively. We exemplify this idea by isolating a fragment of the calculus around the principles of SLL and 4LL. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary lambda-calculi.

ABSTRACT. First-order logic with the reachability predicate (FO(Reach)) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable).

This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a complete characterization of those graph monoids where FO(Reach) is decidable for the resulting transition systems.

ABSTRACT. We show that the coverability problem in ν-Petri nets is complete for `double Ackermann' time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes ν-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals.

ABSTRACT. Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space.