48 citations · 321 across the 68 of their papers we have counts for
61 papers · 1 filter
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…
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…
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.…
Open Higher-Order Logic (Long Version)
Ugo Dal Lago, Francesco Gavazzo, Alexis Ghyselen
We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have a…
On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments (Long Version)
Ugo Dal Lago, Giulia Giusti
A system of session types is introduced as induced by a Curry Howard correspondence applied to Bounded Linear Logic, and then extending the thus obtained type system with probabili…