ABSTRACT. Proof by induction is common-place in mathematics, logic, formal verification, cybersecurity, and many more areas. This talk overviews recent progress in automating inductive reasoning in saturation-based first-order theorem proving. We show how to formalize applications of induction in the saturation process, without bringing drastic changes into the overall framework of first-order proving. We also synthesize code that satisfies a given (inductive) logical specification, while proving the specification in saturation with induction.

ABSTRACT. We introduce a new presentation of the intersection type discipline in which typing judgments derive vectors of types rather than single types. The system uses binary relations to control the flow of information between coordinates of these vectors. We refer to this presentation as system R. The maximal length of type vectors assigned to variables serves as a reasonable notion of dimension for system R, which allows for a natural stratification into fragments of bounded dimension. The present system lies strictly between two known bounded-dimensional systems: the multiset-dimensional system, for which inhabitation is EXPSPACE-complete, and the set-dimensional system, for which inhabitation is undecidable. Our main result is that inhabitation in bounded system R is decidable in 2-EXPTIME, while for each fixed dimension, inhabitation is decidable in EXPTIME. This result is based on a subformula property restricting the inhabitant search space. Unlike in traditional intersection type systems, the proof of the subformula property requires careful treatment of the additional information flow management capabilities. Finally, we argue that system R and its stratification is a valid presentation of the intersection type discipline. First, by proving the subject reduction property for system R in each bounded dimension, and second, by establishing a correspondence with the classical intersection type system of Barendregt, Coppo, and Dezani-Ciancaglini.

ABSTRACT. This paper introduces the hybrid quantum language with general recursion Hyrql, driven towards resource-analysis. By design, Hyrql does not require the specification of an initial set of quantum gates. Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which lead to quantum circuits of distinct complexity. Regarding resource-analysis, we show how to relate the runtime of an expressive fragment of Hyrql programs with the size of the corresponding quantum circuits. We manage to capture the class of functions computable in quantum polynomial time, which, by Yao's Theorem, corresponds to families of circuits of polynomial size. Consequently, this result paves the way for the use of termination and runtime-analysis techniques designed for classical programs to guarantee bounds on the size of quantum circuits.

ABSTRACT. In this paper, we show that the equational theory of relational Kleene algebra with the graph loop operator is PSpace-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this PSpace-completeness still holds by extending with top, tests, converse, and nominals. Notably, by using graph loop and top, we show that for Kleene algebra with tests (KAT), the equational theory of relational KAT with domain is PSpace-complete, resolving a problem left open in previous works, whereas the equational theory of relational KAT with antidomain is ExpTime-complete. To this end, we introduce a novel automaton model on relational structures, named loop-automata. Loop-automata are obtained from non-deterministic finite string automata (NFA) by adding a transition type that tests whether the current vertex has a loop. Using this model, we can give a polynomial-time reduction from the above equational theories to the language inclusion problem for 2-way alternating string automata.

ABSTRACT. Logics of definitions extend first order intuitionistic logic with fixed-point definitions which associate formulas to atomic predicates. These associated formulas must be constrained for consistency. In the original formulation, predicate symbols were required to be ordered and only predicates lower in the order were allowed to appear negatively in the defining formula. This constraint renders ineligible definitions such as those of logical relations in which the predicate being defined must be allowed to appear negatively, albeit with smaller arguments. Tiu has formalized a weaker constraint called ground stratification that permits such definitions and has shown that it suffices for consistency. Definitions can also be given a least fixed-point interpretation via a special induction rule. We address the question of whether Tiu's relaxation carries over to such a treatment. We propose a new induction rule for ground stratified inductive definitions that takes into account the fact that the definition of the predicate in question must itself be considered to be stratified by the complexity of its arguments to obtain a least fixed-point interpretation. We establish the consistency of the resulting logic and we illustrate its new capabilities via an example that encodes a strong normalizability proof for the simply typed $\lambda$-calculus in which the reducibility predicate is inductively defined by recursion on its arguments.

ABSTRACT. While Gentzen’s sequent calculus is a foundational tool for describing and investigating provability, its fine-grained inference rules generally do not directly support automated proof search. While aggregating some introduction rules into synthetic inferences, these do not provide mechanisms for reasoning naturally about the elementary mathematical notions of equivalence and congruence. In this paper, we present a first-order framework for reasoning modulo these relations within the sequent calculus. We provide a setting in which congruences can be treated as actual equalities, mirroring the informal practice of mathematicians and eliminating the need to explicitly use the lemmas typically required for formal congruence proofs. We demonstrate that this approach remains strictly first-order, avoids the complexity of higher-order or set-theoretic constructions, and yields proof systems that retain essential meta-theoretic properties.

ABSTRACT. Reasoning abut equality in calculi that involve binders and structural congruences is challenging because binding and equational theories interact in unexpected and non-obvious ways. We provide a sound and complete proof system to reason about equality modulo alpha-equivalence plus an arbitrary nominal equational theory, generalising nominal algebra by including general permutation fixed-point constraints. We provide examples of application in Milner's pi-calculus, a powerful model of concurrent computation that includes binders and a structural congruence.

ABSTRACT. A standard intensional account of probabilistic computation represents a randomized program as a deterministic computation that consumes an explicit random tape. This yields a two-layer perspective: an intensional layer that makes reuse of randomness and correlation visible, and an extensional layer obtained by interpreting tapes under a chosen probability measure. We develop an evidence-tracked tape semantics using the monadic-core-to-evidenced-frame pipeline (and its induced realizability tripos), obtaining a higher-order logic in which entailments are witnessed by uniform evidence transformers. Quantitative statements are recovered by interpretation: once a tape measure is fixed, probabilities and expectations arise by extracting numerical summaries from tape-indexed predicates, and entailments yield sound inequalities, with an almost-sure quotient supporting probability-one reasoning. We also study intensional principles that are lost at the level of laws, including proof-relevant transport along realizable tape-rewiring maps and a canonical splitting discipline for stream tapes enforcing independent draws. Finally, we relate tape-based reasoning to an extensional law semantics via pushforward, isolating a probability-one must abstraction as a sound summary of tape-based proofs.

ABSTRACT. The (bi)category of profunctors on groupoids is a categorification of the relational model of linear logic. Its objects are not just sets but rather sets whose elements are equipped with groups encoding their symmetries, and its morphisms carry actions by these symmetries. While detailed information on such symmetries helps, e.g., adequacy proofs of profunctorial models, it makes operations such as composition more difficult to compute. A way to ease the computation is to transform a profunctor into a matrix. Although the matrix representation is not functorial in general, it is known to behave well for profunctors definable by \( \lambda \)-terms. The mathematical reason behind this phenomenon, however, was not understood. This paper shows that the key is stability. Stability is a classical concept in domain theory, and has been extended to profunctors in Taylor's work and further developed by Fiore et al. All \( \lambda \)-definable profunctors are known to be stable, and we show that the matrix representation behaves well for stable profunctors. We prove that the matrix representation defines a functor from stable profunctors to matrices that preserves the linear logic structures.

ABSTRACT. Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it generates models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, and more generally in Grothendieck toposes equipped with a tiny proposition. We establish conservativity over Martin-Löf type theory in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.