5 papers · 1 filter
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…
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…
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…