9 papers
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…
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 $Î\vdas…
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 enta…
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…
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…
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…