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 In this paper, we introduce classically time-controlled quantum automata or classically time-controlled quantum automaton (CTQA), which is a reasonable modification of Moore–Crutchfield quantum finite automata that uses time-dependent evolution and a ‘scheduler’ defining how long each Hamiltonian will run. Surprisingly enough, time-dependent evolution provides a significant change in the computational power of quantum automata with respect to a discrete quantum model. Indeed, we show that if a scheduler is not computationally restricted, then a CTQA could even decide the Halting problem. In order to unearth the computational capabilities of CTQAs, we study the case of a computationally restricted scheduler. In particular, we showed that depending on the type of restriction imposed on the scheduler, a CTQA can (i) recognize non-regular languages with cut-point, even in the presence of Karp–Lipton advice, and (ii) recognize non-regular promise languages with bounded-error. Furthermore, we study the cutpoint-union of cutpoint languages by introducing a new model of Moore–Crutchfield quantum finite automata with a rotating tape head. CTQA presents itself as a new model of computation that provides a different approach to a formal study of ‘classical control, quantum data’ schemes in quantum computing.

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.

Abstract We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language.

We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.

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 paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of typing rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi.