2026-07-23T14:09:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25109 2025-12-09T15:09:12Z ddc:004 open_access

Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic Díaz-Caro, Alejandro Malherbe, Octavio Algebraic lambda calculus Categorical semantics Disjunction Proof theory Traditional approaches to modelling parallelism and algebraic structure in lambda calculi often rely on monads - as in Moggi’s framework - or on rich categorical structures such as biproducts - 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: Mag_{Set}, whose objects are magmas and arrows are functions in Set; and AMag^{𝒮}_{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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alejandro Díaz-Caro and Octavio Malherbe 2025 Is Part Of LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2025.28 urn:nbn:de:0030-drops-251098 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.28 eng https://creativecommons.org/licenses/by/4.0/legalcode