ABSTRACT. In this talk we explore the notion of linearisation in the lambda-calculus combining approaches using intersection types and legal paths. We also explore this notion in the broader landscape of substructural type systems. This aims at giving a unified approach in which linearisation is understood as a bridge between semantic path-based models and resource-sensitive type disciplines.

ABSTRACT. We introduce a typing system that is particularly well suited for typing the linear λ -calculus in de Bruijn notation. This typing discipline, which is reminiscent of Hodas’ and Miller’s model of ressource consumption, guarantees that any well-typed term is linear without the need for an occurrence check. We then establish the subject reduction property.

ABSTRACT. Term expansion was originally introduced in 2004 as a way to relate terms typed in an intersection type system with linear terms. Recently, new applications of term expansion include the relation of lambda-terms with terms typed in other substructural type systems, such as the relevant and the ordered type systems, and the use of quantitative types to relate the strongly normalising lambda-terms with weak linear terms that share the same normal form. Here we define a new term expansion for a calculus with explicit substitutions, using it to relate a lambda-calculus with explicit substitutions to Boudol's resource aware lambda-calculus with multiplicities, where function arguments have a possibly limited availability.

ABSTRACT. This paper establishes the cut-elimination theorem for intuitionistic propositional multiplicative-additive linear logic with the least and greatest fixpoints (μIMALL) in terms of its phase semantics. A classical first-order multiplicative-additive linear logic system with the least and greatest fixpoints was introduced in Baelde-Miller (2007). Its intuitionistic fragment was discussed in Baelde (2012), but the cut-elimination theorem for this fragment has not yet been proved. We introduce a propositional fragment of this system, μIMALL, and establish the cut-elimination theorem. To prove the theorem, we define phase semantics for μIMALL and show the following two statements: (1) Soundness: if a formula is provable in μIMALL, then it is true in all phase semantics, and (2) Cut-free Completeness: if a formula is true in all phase semantics, then it is provable in μIMALL without Cut. Okada (1999, 2002) employed a phase semantic method to prove the cut-elimination theorems for classical and intuitionistic linear logic systems. De et al. (2022) applied this method to a propositional fragment of classical propositional multiplicative-additive linear logic with the least and greatest fixpoints. We refine and apply their arguments to prove the cut-elimination theorem for μIMALL.

ABSTRACT. We propose a logical formalisation of computational errors in reactive, non-deterministic systems. To this aim, we introduce a new three-valued symmetric non-deterministic disjunction, designed to provide a faithful logical representation of the non-deterministic choice arising in concurrent computations. The connective is defined within the framework of non-deterministic matrices (Nmatrices) and derives from a minimal combination of Kleene’s tolerant semantics and Bochvar’s symmetric error persistence, thereby eliminating the residual asymmetry induced by sequential evaluation strategies such as McCarthy’s logic. The resulting semantics admits genuinely non-deterministic outcomes in mixed cases involving errors, while preserving commutativity and operational symmetry.

ABSTRACT. The expressivity of session-typed languages has evolved significantly, moving from simple linear protocols to complex systems featuring higher-order polymorphism and context-free structures. However, as the type language grows, defining a robust and decidable notion of type equivalence remains a challenge. We present a novel definition of type equivalence for higher-order polymorphic context-free session types, formulated as a weak bisimulation. The proposed language of types integrates functional and session types, compositional sequencing, and both universal and existential quantification. A distinguishing feature of our framework is the treatment of non-contractivity. Unlike traditional approaches that restrict types to be productive (contractive), we embrace non-contractive types as first-class citizens. We demonstrate that all non-contractive types within a specific kind are behaviorally equivalent; to represent these equivalence classes, we introduce a dedicated Void type. This abstraction allows for a more flexible and uniform treatment of recursion and divergence in session-based communication. To address the practical necessity of type-checking, we prove that our notion of type equivalence is decidable. We achieve this by defining a translation from our type language into a Simple Grammar. By reducing the equivalence problem to the bisimilarity of context-free processes, we leverage existing efficient algorithms to provide a decidable decision procedure. Based on joint work with Andreia Mordido, Diogo Poças, and Vasco T. Vasconcelos.

ABSTRACT. Models of High-level Computation (MHCs) provide effective means to describe complex real-world computing systems because they offer formal foundations for the specification of interacting computing devices, as opposed to describing individual ones, which has been the focus of classical models such as Turing machines or the lambda calculus itself. Despite numerous proposals over the past half century, there is still no canonical MHC akin to Turing machines for (compositionally) reasoning about computation in the large. One of the major drawbacks of state- and data-oriented MHCs is that they extensively neglect control flow, a well-know semantic property that defines computation order. Only control-oriented MHCs treat control explicitly at the expense of ignoring data flow or assuming that data follows control. Mixing data and control within the same framework leads to inefficient methods for formal analysis and verification. To address this, the computon model has recently emerged as a category-theoretic MHC that separates data and control and makes control explicit by supporting composition operators characterised as finite colimit constructions. Such constructions allow the formation of sequential, parallel, branching and iterative computing devices. Unfortunately, the computon model is still a generic reference rather than a concrete realisation. In this paper, we provide a variation of it to enable functional computing devices, introduce a new branching operator, discuss how to define synchronous parallelising out of sequencing and asynchronous parallelising, describe concrete operational semantics for computon execution and provide the first implementation of the model. The implementation yields an open-source programming environment that realises the underlying categorical semantics. This tool is publicly available and ready to build complex computing devices that are structurally correct by construction.

ABSTRACT. Prolog is traditionally thought of as an untyped logic programming language, although there are queries that result in a type error. Several attempts of statically introducing a type discipline in Prolog have been made but they have not been widely adopted. We use Maude to implement a typed unification algorithm and use it as the basis for an interpreter for Prolog called MaudeTypedLog. This interpreter follows the Typed SLD-resolution operational semantics for logic programming, that makes it is possible to detect type errors in both programs and queries dynamically.

ABSTRACT. We study quadrangular properties of binary relations on a set $X$--i.e., properties defined on configurations of four elements—within an agonistic interpretation, where $xRy$ is interpreted as $x$ ``attacks''~$y$. Such relations induce a suitable notion of ``protection,'' and we provide necessary and sufficient conditions for this notion to be consistent. We characterize the balance property in signed frames in terms of a specific quadrangular property, namely collusivity. In this way, we generalize a classical result in balance theory by offering an alternative method for determining whether a network is polarized. That is, one can identify well-formed groups of agents that agree with one another within the same group (a set of allies) while disagreeing with, or attacking, agents outside the group. Furthermore, we extend the balance theorem to non-symmetric relations, thereby relaxing a condition required in standard balance theory. We conclude by giving a modal characterization of collusive frames, together with corresponding rules in a labeled sequent calculus, and we show that previous modal characterizations of balance are derivable within this system.

ABSTRACT. In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), ob- tained via horizontal compression of Natural Deduction proofs in purely implicational minimal logic (M⊃), as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its correctness, showing that the resulting Boolean circuit faithfully characterizes the validity of the encoded DLDS. A Lean formalization establishes machine-checked guarantees of this correspondence, providing a certified link between proof compression and circuit-level verification. This approach opens new perspectives for automated theorem proving and formal certification.