12 citations · 33 across the 10 of their papers we have counts for
10 papers
A quantum let within the lambda calculus
Alejandro Díaz-Caro, Tomás Miguez
Since the seminal work of Selinger and Valiron, the standard design for quantum lambda calculi has kept the quantum state outside the program: terms manipulate pointers to an exter…
Polymorphic System I
Cristian F. Sottile, Alejandro Díaz-Caro, Pablo E. Martínez López
System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an…
A New Connective in Natural Deduction, and its Application to Quantum Computing
Alejandro Díaz-Caro, Gilles Dowek
We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue that these connectiv…
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…
The Vectorial Lambda Calculus Revisited
Francisco Noriega, Alejandro Díaz-Caro
We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) has been originally designed for quantum computing, as an extension to System F w…
Extensional proofs in a propositional logic modulo isomorphisms
Alejandro Díaz-Caro, Gilles Dowek
System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as and , or and $(A\Rightarr…
Runtime Analysis of Quantum Programs: A Formal Approach
Federico Olmedo, Alejandro Díaz-Caro
In this abstract we study the resource consumption of quantum programs. Specifically, we focus on the expected runtime of programs and, inspired by recent methods for probabilistic…
Normalisation of a Non-deterministic Type Isomorphic λ-calculus
Alejandro Díaz-Caro, Gilles Dowek
We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Suc…
Confluence via strong normalisation in an algebraic λ-calculus with rewriting
Pablo Buiras, Alejandro Díaz-Caro, Mauro Jaskelioff
The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axio…
A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron
We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to…