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