19 citations · 74 across the 16 of their papers we have counts for
9 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…
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…
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…
The Sup Connective in IMALL: A Categorical Semantics
Alejandro Díaz-Caro, Octavio Malherbe
We explore a proof language for intuitionistic multiplicative additive linear logic, incorporating the sup connective that introduces additive pairs with a probabilistic eliminatio…
Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
Alejandro Díaz-Caro, Octavio Malherbe
In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives rise to an infinite number of valid typing rules…
A categorical construction for the computational definition of vector spaces
Alejandro Díaz-Caro, Octavio Malherbe
Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other…
A concrete model for a typed linear algebraic lambda calculus
Alejandro Díaz-Caro, Octavio Malherbe
We give an adequate, concrete, categorical-based model for Lambda-S, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-S is an exte…