48 citations · 321 across the 68 of their papers we have counts for
81 papers
Staying Productive Under the Palm Trees: On Graded Coeffect Typing in the Tropical Semiring
Rémy Cerda, Ugo Dal Lago
We show that the tropical semiring over the natural numbers, when used as the grading space in graded coeffect typing, faithfully models the passage of time while simultaneously gu…
On Model-Checking Higher-Order Effectful Programs (Long Version)
Ugo Dal Lago, Alexis Ghyselen
Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be ap…
Contextual Behavioural Metrics (Extended Version)
Ugo Dal Lago, Maurizio Murgia
We introduce contextual behavioural metrics (CBMs) as a novel way of measuring the discrepancy in behaviour between processes, taking into account both quantitative aspects and con…
On the Lattice of Program Metrics
Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone
In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some o…
An Arithmetic Theory for the Poly-Time Random Functions
Melissa Antonelli, Ugo Dal Lago, Davide Davoli +2
We introduce a new bounded theory RS^1_2 and show that the functions which are Sigma^b_1-representable in it are precisely random functions which can be computed in polynomial time…
A Log-Sensitive Encoding of Turing Machines in the -Calculus
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
This note modifies the reference encoding of Turing machines in the -calculus by Dal Lago and Accattoli, which is tuned for time efficiency, as to accommodate logarithmic space.…