3 citations · 8 across the 7 of their papers we have counts for
11 papers
Allegories of Symbolic Manipulations
Francesco Gavazzo
Moving from the mathematical theory of (abstract) syntax, we develop a general relational theory of symbolic manipulation parametric with respect to, and accounting for, general no…
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 Feller Continuity and Full Abstraction (Long Version)
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago +1
We study the nature of applicative bisimilarity in -calculi endowed with operators for sampling from continuous distributions. On the one hand, we show that bisimilarity, logica…
Quantitative and Metric Rewriting: Abstract, Non-Expansive, and Graded Systems
Francesco Gavazzo, Cecilia Di Florio
We introduce a general theory of quantitative and metric rewriting systems, namely systems with a rewriting relation enriched over quantales modelling abstract quantities. We devel…
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…
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (Extended Version)
Francesco Gavazzo
This paper studies the quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value -calculus with…
Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)
Ugo Dal Lago, Francesco Gavazzo, Paul Blain Levy
We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value -calculi with algebraic effects. We first of all endow a computational -calculus with…