Traditional approaches to modelling parallelism and algebraic structure in lambda calculi often rely on monads$\unicode{x2013}$as in Moggi's framework$\unicode{x2013}$or on rich categorical structures such as biproducts$\unicode{x2013}$as used in certain models of linear logic. In this work, we propose a minimal alternative that captures both parallelism and weighted parallelism (linear combinations) within the setting of intuitionistic propositional logic, without resorting to monads or assuming the existence of biproducts. We introduce two lambda calculi: a parallel lambda calculus and an algebraic lambda calculus, both extending full propositional intuitionistic logic. Their semantics are given in two categories: ${\mathbf{Mag}_{\mathbf{Set}}}$, whose objects are magmas and arrows are functions in $\mathbf{Set}$; and ${\mathbf{AMag}^{\mathcal{S}}_{\mathbf{Set}}}$, whose objects are action magmas. The key technical challenge addressed is the interpretation of disjunction in the presence of parallel and algebraic operators. Since the usual coproduct structure is unavailable in our minimal setting, we propose a novel set-theoretic interpretation based on the union of the disjoint union and the Cartesian product. This allows for the construction of sound and adequate models for both calculi. Our results offer a unified and structurally lightweight framework for modelling parallelism and algebraic effects in intuitionistic logic, opening the way to alternatives beyond the traditional monadic or linear logic approaches.

Abstract We introduce the ${{\mathcal L}_!^{\mathcal S}}$-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic. These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the ${{\mathcal L}_{!}^{\mathcal S}}$-calculus as an extension of the ${\mathcal L}^{\mathcal S}$-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalization and an introduction property—as well as preserve the expressiveness of the original ${\mathcal L}^{\mathcal S}$-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.

Abstract We give an adequate, concrete, categorical-based model for Lambda- ${\mathcal S}$ , which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda- ${\mathcal S}$ is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda- ${\mathcal S}$ has a superposition constructor S such that a type A is considered as the base of a vector space, while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over $\mathbb C$ . The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives rise to an infinite number of valid typing rules, without giving preference to any subset of those. In this paper, we introduce a valid subset of typing rules, defining an expressive enough quantum calculus. Then, we propose a categorical semantics for it. Such a semantics consists of an adjunction between the category of distributive-action spaces of value distributions (that is, linear combinations of values in the lambda calculus), and the category of sets of value distributions.

In this work, we continue our consideration of the constructions presented in the paperKrivine's Classical Realizability from a Categorical Perspectiveby Thomas Streicher. Therein, the author points towards the interpretation of the classical realizability of Krivine as an instance of the categorical approach started by Hyland. The present paper continues with the study of the basic algebraic set-up underlying the categorical aspects of the theory. Motivated by the search of a full adjunction, we introduce a new closure operator on the subsets of the stacks of an abstract Krivine structure that yields an adjunction between the corresponding application and implication operations. We show that all the constructions from ordered combinatory algebras to triposes presented in our previous work can be implemented,mutatis mutandis, in the new situation and that all the associated triposes are equivalent. We finish by proving that the whole theory can be developed using the ordered combinatory algebras with full adjunction or strong abstract Krivine structures as the basic set-up.

Abstract In this paper, we continue with the algebraic study of Krivine’s realizability, completing and generalizing some of the authors’ previous constructions by introducing two categories with objects the abstract Krivine structures and the implicative algebras, respectively. These categories are related by an adjunction whose existence clarifies many aspects of the theory previously established. We also revisit, reinterpret, and generalize in categorical terms, some of the results of our previous work such as: the bullet construction, the equivalence of Krivine’s, Streicher’s, and bullet triposes and also the fact that these triposes can be obtained – up to equivalence – from implicative algebras or implicative ordered combinatory algebras.

We propose the new concept ofKrivine ordered combinatory algebra( $\mathcal{^KOCA}$ ) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show that $\mathcal{^KOCA}$ 's are equivalent to Streicher'sabstract Krivine structuresfor the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class oftriposes. The difference between the two representations is that the elements of a $\mathcal{^KOCA}$ play both the role of truth values and realizers, whereas truth values aresetsof realizers in $\mathcal{AKS}$ s. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a $\mathcal{^KOCA}$ , which showcases the dual role that is played by the elements of the $\mathcal{^KOCA}$ .