55 citations
- Consejo Nacional de Investigaciones Científicas y TécnicasAR29 papers
- Universidad de Buenos AiresAR26 papers
- Centre National de la Recherche ScientifiqueFR8 papers
- Universidad de la República de UruguayUY7 papers
- Université de LorraineFR7 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR6 papers
- Institut national de recherche en sciences et technologies du numériqueFR4 papers
- Centre Inria de SaclayFR3 papers
- École PolytechniqueFR3 papers
- Consejo Superior de Investigaciones CientíficasES2 papers
- Délégation Paris 7FR2 papers
- École Normale Supérieure Paris-SaclayFR2 papers
32 papers · 1 filter
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…
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…
Strong normalization through idempotent intersection types: a new syntactical approach
Pablo Barenbaum, Simona Ronchi Della Rocca, Cristian Sottile
It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems r…
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…