2 citations · 4 across the 12 of their papers we have counts for
8 papers · 1 filter
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…