6 papers
When Types Intersect and Effects Get Handled
Stefano Catozi, Ugo Dal Lago, Taro Sekiyama
We introduce a novel intersection type system for a -calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties o…
On Jumps, Interactions, and Intersection Types
Stefano Catozi, Ugo Dal Lago, Gabriele Vanoni
The Jumping Abstract Machine (JAM), an evaluation mechanism for the -calculus, was introduced by Danos and Regnier as an optimization of the Interaction Abstract Machine (IAM),…
On the Metric Nature of (Differential) Logical Relations
Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone
Differential logical relations are methods to measure distances between higher-order programs where distances between functional programs are themselves \emph{functions}, relating…
Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction
Kostia Chardonnet, Ugo Dal Lago, Naohiko Hoshino +1
We present an algorithm turning any term of a linear quantum -calculus into a quantum circuit. The essential ingredient behind the proposed algorithm is Girard's geometry of in…
Linearization via Rewriting (Long Version)
Ugo Dal Lago, Federico Olimpieri
We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time…
On Computational Indistinguishability and Logical Relations
Ugo Dal Lago, Zeinab Galal, Giulia Giusti
A -calculus is introduced in which all programs can be evaluated in probabilistic polynomial time and in which there is sufficient structure to represent sequential cryptograph…