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. 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 work we explore the use of communication actions in a logic aimed to verify authenticity and safety in cryptographic protocols. We extend a Dynamic Logic with Parallel operator by introducing some concepts based on the Dolev-Yao model. The former has a complete axiomatization which yields a complete axiomatization for new the logic being presented. Finally, we also present a tableaux calculus for this logic, proving its termination, soundness and completeness.