ABSTRACT. Approximation semantics capture the observable behaviour of {\lambda}-terms, with Böhm Trees and Taylor Expan- sion standing as two central paradigms. Although conceptually different, these notions are related via the Commutation Theorem, which links the Taylor expansion of a term to that of its Böhm tree. These notions are well understood in Call-by-Name {\lambda}-calculus and have been more recently introduced in Call-by-Value settings. Since these two evaluation strategies traditionally require separate theories, a natural next step is to seek a unified setting for approximation semantics. The Bang-calculus offers exactly such a framework, subsuming both CbN and CbV through linear-logic translations while providing robust rewriting properties. However, its approximation semantics is yet to be fully developed. In this work, we develop the approximation semantics for dBang, the Bang-calculus with explicit substitu- tions and distant reductions. We define Böhm trees and Taylor expansion within dBang and establish their fundamental properties. Our results subsume and generalize Call-By-Name and Call-By-Value through their translations into Bang, offering a single framework that uniformly captures infinitary and resource-sensitive semantics across evaluation strategies.

ABSTRACT. We study invertibility of lambda-terms modulo lambda-theories. Here a fundamental role is played by a class of lambda-terms called finite hereditary permutations (FHP) and by their infinite generalisations (HP). More precisely, FHPs are the invertible elements in the least extensional lambda-theory lambda-eta and HPs are those in the greatest sensible lambda-theory H*. Our approach is based on inverse semigroups, algebraic structures that generalise groups and semilattices. We show that FHP modulo a lambda-theory T is always an inverse semigroup and that HP modulo T is an inverse semigroup whenever T contains the theory of Böhm trees. An inverse semigroup comes equipped with a natural order. We prove that the natural order corresponds to eta-expansion in FHP/T, and to infinite eta-expansion in HP/T. Building on these correspondences we obtain the two main contributions of this work: firstly, we recast in a broader framework the results cited at the beginning; secondly, we prove that the FHPs are the invertible lambda-terms in all the lambda-theories lying between lambda-eta and H+. The latter is Morris' observational lambda-theory, defined by using the beta-normal forms as observables.

ABSTRACT. Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm. We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with eta-equality (Scott, Park, etc.). Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

ABSTRACT. Deduction and static equivalence are central knowledge problems in the formal analysis of security protocols and are known to be undecidable for general equational theories. Several decidable classes have been identified through structural restrictions, including subterm convergent theories, shallow permutative theories, contracting theories and some are implemented in tools such as ProVerif and DeepSec. We identify two recurring themes: symbol preservation, where symbols are maintained across axioms, and symbol contraction, where symbols decrease in depth or number from left to right. For symbol-preserving systems, we introduce measure-invariant (MI) and separate measure-invariant (SMI) theories, generalizing permutative classes and providing new decidable fragments for deduction and static equivalence. Depth-sensitive refinements, including depth-preserving permutative (DPP) and depth-preserving variable-permuting (DPVP) theories, are case studies to understand whether the depth of occurrences of symbols matter. For symbol-contraction systems, we define depth-decreasing (DD) and variable-preserving function-decreasing (VBFD) theories, capturing some simple relaxations of term contraction; while deduction is undecidable in general, these restrictions highlight potential decidable fragments. Overall, our results show that controlling symbol dynamics in rewrite rules provides a unifying perspective on the decidability of knowledge problems, offering conceptual clarity on what makes these problems hard for different equational theories.

ABSTRACT. In this work we prove the undecidability (and Sigma1-completeness) of several theories of semirings with fixed points. The generality of our results stems from recursion theoretic methods, namely the technique of effective inseperability. Our result applies to many theories proposed in the literature, including Conway mu-semirings, Park mu-semirings, and Chomsky algebras.

ABSTRACT. We provide new proofs of two important theorems for proving termination of term rewrite systems (TRSs), including a full formalization in Isabelle/HOL. We first consider Dershowitz' theorem that termination starting from arbitrary terms is equivalent to termination starting from all right-hand sides of the set of right-forward closures, provided that the TRS is right-linear or orthogonal. Our new proof deviates from the original one in that no reorderings of steps in infinite derivations are required, making it more precise in its argumentation. It also subsumes a later result that one can weaken orthogonality to locally confluent overlay TRSs. The second theorem is about matrix interpretations. These were introduced by Hofbauer and Waldmann for proving termination of string rewrite systems (SRSs), internally using the concept of a core. Subsequently, Endrullis, Waldmann and Zantema developed matrix interpretations for TRSs without using the idea of a core. Whereas matrix interpretations for TRSs have already been formalized several times, so far this was not the case for core SRS matrix interpretations. We not only provide such a formalization, but also extend core SRS matrix interpretations to TRSs. These new core matrix interpretations for TRSs generalize previous approaches.

ABSTRACT. Higher-order logic and infinitary logic are two extensions of first-order logic that allow greater expressivity. Both features have not been investigated together yet. In this paper, we define a higher-order infinitary logic, based on an extension of simple type theory. The resulting logic features higher-order quantifiers, infinite conjunction and infinite disjunction. We establish results at both the syntactic and the semantic level. We introduce a sound notion of model, and we show a strong version of completeness that entails the cut-elimination theorem for natural deduction. Moreover, we prove an extension of Barr's theorem, allowing us to constructivize classical proofs of a particular fragment of higher-order infinitary logic.

ABSTRACT. DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.