2 citations · 4 across the 12 of their papers we have counts for
12 papers
Basis-Sensitive Quantum Typing via Realisability
Alejandro Díaz-Caro, Octavio Malherbe, Rafael Romero
We present , a quantum-control -calculus that refines previous basis-sensitive systems by allowing abstractions to be expressed with respect to arbitrary -- possibly entang…
Proceedings of the 22nd International Conference on Quantum Physics and Logic
Alejandro Díaz-Caro, Ognyan Oreshkov, Ana Belén Sainz
This volume contains the proceedings of the 22nd International Conference on Quantum Physics and Logic (QPL 2025), which was held from 14th to 18th July 2025, in Varna, Bulgaria, o…
A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
Alejandro Díaz-Caro, Nicolas A. Monzon
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, Lamb…
IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
Kinnari Dave, Alejandro Díaz-Caro, Vladimir Zamdzhiev
We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality B to capture mixed-state quantum computation. The language s…
Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
Alejandro Díaz-Caro
This invited paper presents an overview of an ongoing research program aimed at extending the Curry-Howard-Lambek correspondence to quantum computation. We explore two key framewor…
Expectation-based Analysis of Higher-Order Quantum Programs
Martin Avanzini, Alejandro Díaz-Caro, Emmanuel Hainry +1
The paper extends the expectation transformer based analysis of higher-order probabilistic programs to the quantum higher-order setting. The quantum language we are considering can…
An Algebraic Extension of Intuitionistic Linear Logic: The -Calculus and Its Categorical Model
Alejandro Díaz-Caro, Malena Ivnisky, Octavio Malherbe
We introduce the -calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic (IL…
A new introduction rule for disjunction
Alejandro Díaz-Caro, Gilles Dowek
We extend Natural Deduction for intuitionistic logic with a third introduction rule for the disjunction, -i3, with a conclusion , but both premises $Γ\vdash…
Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic
Alejandro Díaz-Caro, Octavio Malherbe
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 ca…
A feasible and unitary quantum programming language
Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux +1
We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boa…
A linear proof language for second-order intuitionistic linear logic
Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky +1
We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling…
A General Probabilistic Framework in IMALL: A Concrete Categorical Perspective
Alejandro Díaz-Caro, Octavio Malherbe
We consider the linear lambda-calculus extended with the sup type constructor, which provides an additive conjunction along with a non-deterministic destructor. The sup type constr…