19 citations · 74 across the 16 of their papers we have counts for
17 papers
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…
The category of implicative algebras and realizability
Walter Ferrer, Octavio Malherbe
In this paper we continue with the algebraic study of Krivine's realizability, refining some of the authors' previous constructions by introducing two categories, with objects the…
Linear Hyperdoctrines and Comodules
Mariana Haim, Octavio Malherbe
In this exposition, we get examples of what is called a "linear hyperdoctrine", based on categories of comodules indexed by coalgebras. This structures can model first order linear…
Realizability in OCAs and AKSs
Walter Ferrer Santos, Mauricio Guillermo, Octavio Malherbe
In the context of the associated to an we introduce a closure operator and two associated maps that replace the closure and the maps defined in \c…
Ordered combinatory algebras and realizability
Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo +2
We consider different classes of combinatory structures related to Krivine realizability. We show, in the precise sense that they give rise to the same class of triposes, that they…
A Report on Realizability
Walter Ferrer Santos, Mauricio Guillermo, Octavio Malherbe
Besides recalling the basic definitions of Realizability Lattices, Abstract Krivine Structures, Ordered Combinatory Algebras and Tripos and reviewing its relationships, we propose…
Presheaf models of quantum computation: an outline
Octavio Malherbe, Philip Scott, Peter Selinger
This paper outlines the construction of categorical models of higher-order quantum computation. We construct a concrete denotational semantics of Selinger and Valiron's quantum lam…
Categorical models of computation: partially traced categories and presheaf models of quantum computation
Octavio Malherbe
This dissertation has two main parts. The first part deals with questions relating to Haghverdi and Scott's notion of partially traced categories. The main result is a representati…
Partially traced categories
Octavio Malherbe, Philip J. Scott, Peter Selinger
This paper deals with questions relating to Haghverdi and Scott's notion of partially traced categories. The main result is a representation theorem for such categories: we prove t…