Mid-term Meeting: QCOMICAL Project

The Mid-term Meeting of the QCOMICAL project will take place virtually (on Google Meet) on March 31, 2026. This meeting serves as a key milestone to review progress, coordinate upcoming secondments, and discuss scientific advancements within the work packages.

Program

---

Abstracts

• Mario Silva: Quantum Programming in Polylogarithmic Time

Polylogarithmic time delineates a relevant notion of feasibility on several classical computational models such as Boolean circuits or parallel random access machines. As far as the quantum paradigm is concerned, this notion yields the complexity class FBQPOLYLOG of functions approximable in polylogarithmic time with a quantum random access Turing machine. We introduce a quantum programming language with first-order recursive procedures, which provides the first programming language-based characterization of FBQPOLYLOG. Each program computes a function in FBQPOLYLOG (soundness) and, conversely, each function of this complexity class is computed by a program (completeness). We also provide a compilation strategy from programs to uniform families of quantum circuits of polylogarithmic depth and polynomial size, whose set of computed functions is known as QNC, and recover the well-known separation result FBQPOLYLOG ⊊ QNC.

• Malena Ivnisky: An Algebraic Extension of Intuitionistic Linear Logic: the L-S-!-Calculus and Its Categorical Model

We introduce the L-S-!-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic (ILL). 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 L-S-!-calculus as an extension of the L-S-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalisation, and an introduction property—as well as preserve the expressiveness of the original L-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 quantum programming language grounded in linear logic.

• Nicolás Monzón: A Quantum-Control Lambda-Calculus with Multiple Measurement Bases

We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements. We formalise its syntax, typing rules, subtyping, and operational semantics, and establish its key meta-theoretical properties. This proof-of-concept shows that support for multiple bases can be coherently integrated into the type discipline of quantum programming languages.

• Octave Mestoudjian: Picturing General Quantum Subsystems

We extend the usual process-theoretic view on locality and causality in subsystems (based on the tensor product case) to general quantum systems (i.e. possibly non-factor, finite-dimensional von Neumann algebras). To do so, we introduce a primitive notion of splitting maps within dagger symmetric monoidal categories. Splitting maps give rise to subsystems that admit comparison via a preorder called comprehension, and support an adaptation of the usual categorical trace. We show that the comprehension preorder precisely captures the inclusion partial order between von Neumann algebras, and that the splitting map trace captures the natural notion of von Neumann algebra trace. As a consequence of the development of these diagrammatic tools, we prove that the known equivalence between semi-causality and semi-localisability for factor subsystems extends to all (including non-factor) subsystems.