1 citations · 1 across the 2 of their papers we have counts for
7 papers
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 Reinforcement Learning, Effect Handlers, and the State Monad
Ugo Dal Lago, Francesco Gavazzo, Alexis Ghyselen
We study the algebraic effects and handlers as a way to support decision-making abstractions in functional programs, whereas a user can ask a learning algorithm to resolve choices…
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Systems
Ugo Dal Lago, Francesco Gavazzo
We investigate program equivalence for linear higher-order(sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based…
Modal Reasoning = Metric Reasoning, via Lawvere
Ugo Dal Lago, Francesco Gavazzo
Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent computations where code usage plays a central role. The theory of program…
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…
Differential Logical Relations, Part I: The Simply-Typed Case (Long Version)
Ugo Dal Lago, Francesco Gavazzo, Akira Yoshimizu
We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a b…