48 citations · 321 across the 68 of their papers we have counts for
7 papers · 1 filter
The (In)Efficiency of Interaction
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce efficiencies, the price being…
Intersection Types and (Positive) Almost-Sure Termination
Ugo Dal Lago, Claudia Faggian, Simona Ronchi Della Rocca
Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice…
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago +1
Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order…
Decomposing Probabilistic Lambda-calculi
Ugo Dal Lago, Giulio Guerrieri, Willem Heijltjes
A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these st…
On Higher-Order Cryptography (Long Version)
Boaz Barak, Raphaëlle Crubillé, Ugo Dal Lago
Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-…
The Abstract Machinery of Interaction (Long Version)
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine,…
A Diagrammatic Calculus for Algebraic Effects
Ugo Dal Lago, Francesco Gavazzo
We introduce a new diagrammatic notation for representing the result of (algebraic) effectful computations. Our notation explicitly separates the effects produced during a computat…