ABSTRACT. Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical representation of omega-regular languages. The co-Büchi automata in a chain assign each omega-word its natural color, which depends only on the language itself and not on the chosen automaton representation. Automata in such a chain can be minimized in polynomial time and are good-for-games, making this representation attractive for verification and reactive synthesis. However, in these applications, specifications are usually given in linear temporal logic (LTL). To make COCOA useful, an LTL specification must first be translated into the chain of automata. The only translation currently known proceeds via deterministic parity automata (LTL → DPA → COCOA), where the first step ignores natural colors and requires intricate constructions due to Safra or Esparza et al. This raises the question of whether, by exploiting the definition of the natural color of words, one can avoid these complex constructions and obtain a more direct translation from LTL to COCOA. In this paper, we present a simple yet optimal translation from LTL to COCOA, as well as a variant that translates LTL into DPA. The translation represents a new route from LTL to DPA and avoids the aforementioned intricate constructions. It relies on standard operations on weak alternating automata, Miyano-Hayashi's breakpoint construction, the subset construction, and simple graph algorithms. Starting from weak alternating automata, the procedure also applies to specifications in linear dynamic logic. The procedure runs in asymptotically optimal doubly exponential time and produces automata of asymptotically optimal size.

ABSTRACT. We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that for layered automata both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences.

ABSTRACT. We study the uniformisation problem for monadic second-order logic (MSO) over countable ordinal chains, ie, given a formula that refines a relation between subsets of the input model, we are interested in the existence of a formula that defines a function that selects for all sets in the domain of the relation a unique set such that the pair of the two is in the relation. It is known that uniformisation of MSO is not possible over the class of countable ordinals. We show in this work that the maximal uniformisation degree is reached if we add to the logic a new predicate that selects in each set, if possible, a cofinal subset of a of order-type $\omega$. Said differently, all formulas of MSO can be uniformised over the class of countable ordinal chains by using a formula of this extended logic.

ABSTRACT. Rabin's Tree Theorem says that the MSO theory of the infinite binary tree $2^*$ is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to $2^{\leq \omega}$, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in $2^{\leq \omega}$ by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin's Theorem can be extended to the new framework. The only missing part is a conjecture about finite memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games.

ABSTRACT. We propose a simple space-cost measure for the lambda-calculus, that extends the natural model measuring the size of the terms by also taking into consideration their origin. This new model is able to capture sublinear space complexity and we prove that, in the context of weak reduction, it is reasonable with respect to standard complexity theory. Precisely, we show that the weak lambda-calculus and Turing machines can simulate each other with a constant-factor space overhead, for any computation of logarithmic or higher space complexity. This implies that the weak lambda-calculus equipped with our cost model gives a proper characterization of the classical space complexity classes, including LOGSPACE and PSPACE.

ABSTRACT. Semantic notions in programming language theory are commonly specified by syntax-based systems, and their metatheory --- including congruence of bisimilarity, determinacy of evaluation, confluence of reduction, and type safety --- is typically developed syntactically, relying heavily on termwise reasoning. This leads to representation-dependent results and to a systematic duplication of metatheoretic effort across different calculi and syntactic presentations. This paper proposes a pointfree, algebraic approach to the metatheory of syntax-based systems. Rather than reasoning about terms, inference mechanisms, or other syntactic notions --- or about their abstract structure --- we shift attention to the algebra of semantic predicates induced by syntax and treat such predicates as first-class objects. This algebra is defined abstractly, without reference to any underlying term structure. Term-based rules and manipulations are recast as algebraic operations, while metatheoretic properties are formulated algebraically --- typically as quasi-equations --- and established once and for all at the algebraic level, independently of any particular syntactic representation. As a first step towards a systematic algebraization of metatheory, we prove a collection of abstract metatheorems, including confluence of reduction, determinacy of evaluation, and congruence of applicative bisimilarity.

ABSTRACT. Friedman-Simpson’s original program of reverse mathematics, as is also the case for most of standard mathematics, has been developed in classical subsystems of second-order arithmetic. As such, (classical) reverse mathematics presents various limitations from a constructive point of view, since for instance they are unable do distinguish between a statement and its contrapositive (e.g. dependent choice and the bar induction principles). The case of (Weak) König Lemma (WKL) and Fan Theorem (FT) is particularly interesting in that regard: while KL is well-known to imply FT, and if constructivists like Brouwer rejected the former while admitting the latter, the converse implication has not been much studied for years. It is only recently that a growing enthusiasm for constructive reverse mathematics pushed towards a finer-grained analysis of the connection between such principles. In addition to intuitionistic reverse mathematics, the realizability approach to logical principles adds a computational meaning to purely logical statements. We follow this path to investigate the computational meaning to Brouwer's Fan Theorem: building on recent work by Lubarsky and Rathjen, we first construct a realizability interpretation of higher-order logic validating FT while refuting WKL. This interpretation relies on a λ-calculus extended with oracles while preserving a notion of continuity for realizers. We then push this approach a step further to show the robustness of this realizability interpretation by identifying, in the abstract and general setting of evidenced frames, sufficient computational conditions entailing FT.

ABSTRACT. Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as $\lambda$-terms. One distinguishing feature of the presheaf-based perspective is its abstract syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, modelling substitution in the spirit of Fiore~et.~al.'s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from an action. We then demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories, but also yields novel notions of substitution tensor for nominal sets and their relatives, such as renaming sets. Our results also shed new light on the relation between presheaves and nominal sets, in which we establish novel correspondences between different versions of nominal sets and suitable (pre-)sheaf categories.

ABSTRACT. The logic of bunched implications (BI), introduced by O’Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the $\{\land, \lor, \neg, \mimp\}$-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then $\mimp$ splits into two divisions $\backslash, \slash$). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.

ABSTRACT. Substructural logics selectively omit structural rules from classical or intuitionistic proof calculi, providing a framework to formalize resource-sensitive reasoning. For logics with contraction or weakening admitting cut-free sequent calculi, proof search had been analyzed in the literature using well-quasi-orders on N^d (Dickson’s lemma), yielding Ackermannian upper bounds via controlled bad-sequence arguments. For hypersequent calculi, that argument lifted the ordering to the powerset, since a hypersequent is a (multi)set of sequents. From the perspective of the fast-growing hierarchy, this induced a jump from Ackermannian to hyper-Ackermannian complexity. This suggested that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening (FLec/FLew) inherently entail hyper-Ackermannian upper bounds. We show that this intuition does not hold: every extension of FLec and FLew admitting a cut-free hypersequent calculus has an Ackermannian upper bound on provability. The key technical insight is avoiding the powerset. For this, we exploit novel dependencies between individual sequents within any hypersequent in backward proof search. The weakening case also introduces a Karp-Miller style acceleration. Our Ackermannian upper bound is optimal (realized by the logic FLec), and it improves the upper bound for the fundamental fuzzy logic MTL.

ABSTRACT. Subtyping in programming languages can be analysed as an entailment relation by means of proof theory. We look at two main families of systems: intersection types and polymorphic subtyping. We introduce a restriction IS of the Lambek calculus which is stable under cut-elimination and conservatively extends these two subtyping relations. IS is an intuitionistic non-commutative linear sequent calculus which provides a natural logical setting for the study of subtyping. We recover sequent calculi from the literature as restrictions of IS (thanks to a proof-theoretical analysis: admissibility, invertibility, focusing, etc.), so that IS appears as a unifying logic. We also develop translations relating IS with relevant logic, (unconstrained) Lambek or cyclic linear logic.

ABSTRACT. History-deterministic automata, often also known as good-for-games, are an intermediate model between deterministic and nondeterministic automata, which are particularly well-suited for applications in verification and reactive synthesis. We show that deciding whether a parity automaton is history-deterministic is in NP. Our result matches an NP-hardness lower bound (Prakash 2024) and builds on insights from a fixed-parameter tractable algorithm (Lehtinen and Prakash 2025). This settles the complexity of the problem, which has been open since 2006.

ABSTRACT. We consider a large family of product operations of formal power series in noncommuting indeterminates, the classes of automata they define, and the respective equivalence problems. A \emph{$P$-product} of series is defined coinductively by a \emph{polynomial product rule $P$}, which gives a recursive recipe to build the product of two series as a function of the series themselves and their derivatives. The first main result of the paper is a complete and decidable characterisation of all product rules $P$ giving rise to $P$-products which are bilinear, associative, and commutative. The characterisation shows that there are infinitely many such products, and in particular it applies to the notable Hadamard, shuffle, and infiltration products from the literature. Every $P$-product gives rise to the class of \emph{$P$-automata}, an infinite-state model where states are terms. The second main result of the paper is that the equivalence problem for $P$-automata is decidable for $P$-products satisfying our characterisation. This explains, subsumes, and extends known results from the literature on the Hadamard, shuffle, and infiltration automata. We have formalised most results in the proof assistant Agda.

ABSTRACT. We provide general criteria ensuring the existence of minimal canonical models of streaming transducers, namely, devices that read an input word and produce a corresponding output value by iteratively updating an internal memory. This abstract model of transducer subsumes classical (sub)sequential transducers (Schützenberger), streaming string-to-string transducers (Alur-Černý), polynomial automata (Benedikt et al.), and variants of streaming string-to-tree transducers (Alur-D'Antoni). We then instantiate our criteria to minimize variants of the latter transducers, where outputs are terms that are constructed incrementally, by extending (tuples of) terms either at the leaves or at the roots.

ABSTRACT. The determinisation problem for min-plus (tropical) weighted automata was recently shown to be decidable. However, the proof is purely existential, relying on several non-constructive arguments. Our contribution in this work is twofold: first, we present the first complexity bound for this problem, showing it is primitive recursive. Second, our techniques introduce a versatile framework to analyse runs of weighted automata in a constructive manner. In particular, this significantly simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.

ABSTRACT. In this paper we introduce the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata (over a field) by allowing the transition weights to be rational functions of the tree size. Whereas the class of generating functions of weighted tree automata coincides with the class of algebraic power series, our main result is that that the class of generating functions of differential tree automata coincides with the class of differentially algebraic power series. As a corollary, we obtain a decision procedure for determining equivalence of differential tree automata. In the course of proving our main result we identify a class of recurrences that characterises the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. We further identify a natural syntactic subset of differential tree automata whose generating functions are given by rational dynamical systems, that is, as components of the solution of a system of differential equations $\boldsymbol{y}' = F(\boldsymbol y)$, where $F$ is a vector of rational functions that is defined at $\boldsymbol y(0)$. We further show that this class of power series can be characterised in terms of the classical notion of weighted tree automata by using a labelled generating function on trees.

ABSTRACT. Hofmann (1999) introduced the functional programming language LFPL to characterize the functions computable in polynomial time using an affine type system. LFPL enables a natural programming style, including nested recursion, and has inspired the development of type systems for automatic cost analysis, linear dependent type theories, and efficient memory management in functional programming languages. Despite its prominence, there does not exist a self-contained presentation, let alone a full mechanization, of LFPL and its core metatheory. This article presents a modern account and mechanization of LFPL and its metatheory with the goal of being self-contained and accessible while streamlining the strongest-known soundness and completeness results. The soundness proof works with the language LFPL+, which extends LFPL with additional language features. The proof is novel, adapting a technique by Aehlig and Schwichtenberg (2002) to construct explicit polynomials that bound the cost of an LFPL+ expression with respect to a big-step cost semantics. The completeness proof shows that LFPL programs can simulate polynomial-time Turing machines while only relying on restricted forms of linear functions and lists. It has the same structure as the original proof by Hofmann (2002) but greatly simplifies the core argument with a novel stack-like data structure that is implemented with first-class functions and lists. The mechanization includes the full soundness and completeness proofs, and serves as one of the first case studies of mechanized metatheory in the recently developed proof assistant Istari.

ABSTRACT. 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 Layered Modal ML (LMML), \textit{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 LMML, establishing \textit{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.