Ugo Dal Lago

TCS Journal 2026 Journal Article

(Definitely not) Boring interaction abstract machines

• Ugo Dal Lago
• Gabriele Vanoni

The interaction abstract machine is an automata-theoretic implementation of Girard’s geometry of interaction. We study one of its two formulations for the λ -calculus, namely the one obtained from the so-called call-by-value (or “boring”) translation of intuitionistic logic into linear logic. We prove the correctness of the resulting call-by-name machine, at the same time establishing an improvement bisimulation with Krivine’s abstract machine. The proof makes essential use of the definition of a novel relational property linking configurations of the two machines. Finally, exploiting the correspondence with non-idempotent intersection types, we prove that the interaction abstract machines coming from Girard’s two translations are strongly bisimilar.

FSCD Conference 2025 Conference Paper

On the Metric Nature of (Differential) Logical Relations

• Ugo Dal Lago
• Naohiko Hoshino
• Paolo Pistone

Differential logical relations are a method to measure distances between higher-order programs. They differ from standard methods based on program metrics in that differences between functional programs are themselves functions, relating errors in input with errors in output, this way providing a more fine grained, contextual, information. The aim of this paper is to clarify the metric nature of differential logical relations. While previous work has shown that these do not give rise, in general, to (quasi-)metric spaces nor to partial metric spaces, we show that the distance functions arising from such relations, that we call quasi-quasi-metrics, can be related to both quasi-metrics and partial metrics, the latter being also captured by suitable relational definitions. Moreover, we exploit such connections to deduce some new compositional reasoning principles for program differences.

CSL Conference 2024 Conference Paper

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories

• Melissa Antonelli
• Ugo Dal Lago
• Davide Davoli 0001
• Isabel Oitavem
• Paolo Pistone

We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T, where T = IΔ₀+Exp is a well-studied theory based on bounded induction.

TCS Journal 2024 Journal Article

Preface

• Ugo Dal Lago
• Daniele Gorla

TCS Journal 2023 Journal Article

On counting propositional logic and Wagner's hierarchy

• Melissa Antonelli
• Ugo Dal Lago
• Paolo Pistone

We introduce an extension of classical propositional logic with counting quantifiers. These forms of quantification make it possible to express that a formula is true in a certain portion of the set of all its interpretations. Beyond providing a sound and complete proof system for this logic, we show that validity problems for counting propositional logic can be used to capture counting complexity classes. More precisely, we show that the complexity of the decision problems for validity of prenex counting formulas perfectly matches the appropriate levels of Wagner's counting hierarchy.

FSCD Conference 2023 Conference Paper

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 of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i. e. , whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i. e. , the denotational and interactive ones, lie in between the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz.

CSL Conference 2023 Conference Paper

Open Higher-Order Logic

• 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 an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function’s domain of definition.

FSCD Conference 2022 Conference Paper

On Quantitative Algebraic Higher-Order Theories

• Ugo Dal Lago
• Furio Honsell
• Marina Lenisa
• Paolo Pistone

We explore the possibility of extending Mardare et al. ’s quantitative algebras to the structures which naturally emerge from Combinatory Logic and the λ-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results clearly delineating to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras.

MFCS Conference 2021 Conference Paper

A Recursion-Theoretic Characterization of the Probabilistic Class PP

• Ugo Dal Lago
• Reinhard Kahle
• Isabel Oitavem

Probabilistic complexity classes, despite capturing the notion of feasibility, have escaped any treatment by the tools of so-called implicit-complexity. Their inherently semantic nature is of course a barrier to the characterization of classes like BPP or ZPP, but not all classes are semantic. In this paper, we introduce a recursion-theoretic characterization of the probabilistic class PP, using recursion schemata with pointers.

TCS Journal 2021 Journal Article

Differential logical relations, part II increments and derivatives

• Ugo Dal Lago
• Francesco Gavazzo

We study the deep relation existing between differential logical relations and incremental computing by showing how self-differences in the former precisely correspond to derivatives in the latter. The byproduct of such a relationship is twofold: on the one hand, we show how differential logical relations can be seen as a powerful meta-theoretical tool in the analysis of incremental computations, enabling an easy proof of soundness of differentiation. On the other hand, we generalize differential logical relations so as to be able to interpret full recursion, something not possible in the original system.

FSCD Conference 2021 Conference Paper

Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs

• 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 notions of program equivalence for a linear λ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.

TCS Journal 2020 Journal Article

Effectful applicative similarity for call-by-name lambda calculi

• Ugo Dal Lago
• Francesco Gavazzo
• Ryo Tanaka

We introduce a notion of applicative similarity in which not terms but monadic values arising from the evaluation of effectful terms, can be compared. We prove this notion to be fully abstract whenever terms are evaluated in call-by-name order. This is the first full-abstraction result for such a generic, coinductive methodology for program equivalence.

TCS Journal 2020 Journal Article

On randomised strategies in the λ-calculus

• Ugo Dal Lago
• Gabriele Vanoni

In this work we study randomised reduction strategies—a notion already known in the context of abstract reduction systems—for the λ-calculus. We develop a simple framework that allows us to prove a randomised strategy to be positive almost-surely normalising. Then we propose a simple example of randomised strategy for the λ-calculus that has such a property and we show why it is non-trivial with respect to classical deterministic strategies such as leftmost-outermost or rightmost-innermost. We conclude studying this strategy for two sub-λ-calculi, namely those where duplication and erasure are syntactically forbidden, showing some non-trivial properties.

FSCD Conference 2020 Conference Paper

Solvability in a Probabilistic Setting (Invited Talk)

• Simona Ronchi Della Rocca
• Ugo Dal Lago
• Claudia Faggian

The notion of solvability, crucial in the λ-calculus, is conservatively extended to a probabilistic setting, and a complete characterization of it is given. The employed technical tool is a type assignment system, based on non-idempotent intersection types, whose typable terms turn out to be precisely the terms which are solvable with nonnull probability. We also supply an operational characterization of solvable terms, through the notion of head normal form, and a denotational model of Λ_⊕, itself induced by the type system, which equates all the unsolvable terms.

I&C Journal 2018 Journal Article

On sharing, memoization, and polynomial time

• Martin Avanzini
• Ugo Dal Lago

We study how the adoption of an evaluation mechanism with sharing and memoization impacts the class of functions which can be computed in polynomial time. We first show how a natural cost model in which lookup for an already computed result has no cost is indeed invariant. As a corollary, we then prove that the most general notion of ramified recurrence is sound for polynomial time, this way settling an open problem in implicit computational complexity.

I&C Journal 2016 Journal Article

Computation by interaction for space-bounded functional programming

• Ugo Dal Lago
• Ulrich Schöpp

When programming with sublinear space constraints one often needs to use special implementation techniques even for simple tasks, such as function composition. In this paper, we study how such implementation techniques can be supported in a functional programming language. Our approach is based on modelling computation by interaction using the Int construction of Joyal, Street & Verity. We apply this construction to a term model of a first-order programming language and use the resulting structure to derive the functional programming language intml. Intml can be understood as a programming language simplification of Stratified Bounded Affine Logic. We formulate intml by means of a type system inspired by Baillot & Terui's Dual Light Affine Logic. We show that it captures the complexity classes flogspace and nflogspace. We illustrate its expressiveness by showing how typical graph algorithms, such a test for acyclicity in undirected graphs, can be represented.

I&C Journal 2016 Journal Article

Higher-order interpretations and program complexity

• Patrick Baillot
• Ugo Dal Lago

Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs [10]. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider simply-typed term rewriting systems [35], we define higher-order polynomial interpretations for them, and we give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.

I&C Journal 2015 Journal Article

A higher-order characterization of probabilistic polynomial time

• Ugo Dal Lago
• Paolo Parisen Toldin

We present RSLR, an implicit higher-order characterization of the class PP of those problems which can be decided in probabilistic polynomial time with error probability smaller than 1 2. Analogously, a (less implicit) characterization of the class BPP can be obtained. RSLR is an extension of Hofmann's SLR with a probabilistic primitive, which enjoys basic properties such as subject reduction and confluence. Polynomial time soundness of RSLR is obtained by syntactical means, as opposed to the standard literature on SLR -derived systems, which use semantics in an essential way.

TCS Journal 2015 Journal Article

Developments in Implicit Complexity (DICE 2012)

• Ugo Dal Lago
• Guillaume Bonfante

LPAR Conference 2015 Conference Paper

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

• Patrick Baillot
• Gilles Barthe
• Ugo Dal Lago

Abstract We define a call-by-value variant of Gödel’s System \(\mathsf {T} \) with references, and equip it with a linear dependent type and effect system, called \(\mathsf {d}\ell \mathsf {T} \), that can estimate the complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, in the sense that it over-approximates the complexity of executing the programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of \(\mathsf {d}\ell \mathsf {T} \). Finally, we demonstrate the usefulness of \(\mathsf {d}\ell \mathsf {T} \) for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich-Levin theorem.

LPAR Conference 2013 Conference Paper

Complexity Analysis in Presence of Control Operators and Higher-Order Functions

• Ugo Dal Lago
• Giulio Pellitta

Abstract A polarized version of Girard, Scedrov and Scott’s Bounded Linear Logic is introduced and its normalization properties studied. Following Laurent [25], the logic naturally gives rise to a type system for the λμ -calculus, whose derivations reveal bounds on the time complexity of the underlying term. This is the first example of a type system for the λμ -calculus guaranteeing time complexity bounds for typable programs.

CSL Conference 2012 Conference Paper

Higher-Order Interpretations and Program Complexity

• Patrick Baillot
• Ugo Dal Lago

Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider the notion of simply-typed term rewriting systems, we define higher-order polynomial interpretations for them and give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.

I&C Journal 2011 Journal Article

Light logics and optimal reduction: Completeness and complexity

• Patrick Baillot
• Paolo Coppola
• Ugo Dal Lago

Typing of lambda-terms in elementary and light affine logic (EAL and LAL, respectively) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, respectively) proof-nets admits a guaranteed polynomial (elementary, respectively) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping’s algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL, respectively) typed terms, Lamping’s abstract algorithm also admits a polynomial (elementary, respectively) bound. We also give a proof of its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics).

TCS Journal 2011 Journal Article

Realizability models and implicit complexity

• Ugo Dal Lago
• Martin Hofmann

New, simple, proofs of soundness (every representable function lies in a given complexity class) for Elementary Affine Logic, LFPL and Soft Affine Logic are presented. The proofs are obtained by instantiating a semantic framework previously introduced by the authors and based on an innovative modification of realizability. The proof is a notable simplification on the original already semantic proof of soundness for the above mentioned logical systems and programming languages. A new result made possible by the semantic framework is the addition of polymorphism and a modality to LFPL, thus allowing for an internal definition of inductive datatypes. The methodology presented proceeds by assigning both abstract resource bounds in the form of elements from a resource monoid and resource-bounded computations to proofs (respectively, programs).

TCS Journal 2010 Journal Article

Quantum implicit computational complexity

• Ugo Dal Lago
• Andrea Masini
• Margherita Zorzi

We introduce a quantum lambda calculus inspired by Lafont’s Soft Linear Logic and capturing the polynomial quantum complexity classes EQP, BQP and ZQP. The calculus is based on the “classical control and quantum data” paradigm. This is the first example of a formal system capturing quantum complexity classes in the spirit of implicit computational complexity — it is machine-free and no explicit bound (e. g. , polynomials) appears in its syntax.

CSL Conference 2008 Conference Paper

Quantitative Game Semantics for Linear Logic

• Ugo Dal Lago
• Olivier Laurent 0001

Abstract We present a game-based semantic framework in which the time complexity of any IMELL proof can be read out of its interpretation. This gives a compositional view of the geometry of interaction framework introduced by the first author. In our model the time measure is given by means of slots, as introduced by Ghica in a recent paper. The cost associated to a strategy is polynomially related to the normalization time of the interpreted proof, in the style of a complexity-theoretical full abstraction result.

TCS Journal 2008 Journal Article

The weak lambda calculus as a reasonable machine

• Ugo Dal Lago
• Simone Martini

We define a new cost model for the call-by-value lambda-calculus satisfying the invariance thesis. That is, under the proposed cost model, Turing machines and the call-by-value lambda-calculus can simulate each other within a polynomial time overhead. The model only relies on combinatorial properties of the usual beta-reduction, without any reference to a specific machine or evaluator. In particular, the cost of a single beta reduction is proportional to the difference between the size of the redex and the size of the reduct. In this way, the total cost of normalizing a lambda term will take into account the size of all intermediate results (as well as the number of steps to normal form).

TCS Journal 2007 Journal Article

Compact and tractable automaton-based representations of time granularities

• Ugo Dal Lago
• Angelo Montanari
• Gabriele Puppis

Most approaches to time granularity proposed in the literature are based on algebraic and logical formalisms [J. Euzenat, A. Montanari, Time granularity, in: M. Fisher, D. Gabbay, L. Vila (Eds.), Handbook of Temporal Reasoning in Artificial Intelligence, Elsevier, 2005, pp. 59–118]. Here we follow an alternative automaton-based approach, originally outlined in [U. Dal Lago, A. Montanari, Calendars, time granularities, and automata, in: Proceedings of the 7th International Symposium on Spatial and Temporal Databases, SSTD, in: LNCS, vol. 2121, Springer, 2001, pp. 279–298], which makes it possible to deal with infinite time granularities in an effective and efficient way. Such an approach provides a neat solution to fundamental algorithmic problems, such as the granularity equivalence and granule conversion problems, which have been often neglected in the literature. In this paper, we focus our attention on two basic optimization problems for the automaton-based representation of time granularities, namely, the problem of computing the smallest representation of a time granularity and that of computing the most tractable representation of it, that is, the one on which crucial algorithms, such as granule conversion algorithms, run fastest.

TIME Conference 2007 Conference Paper

On the Equivalence of Automaton-Based Representations of Time Granularities

• Ugo Dal Lago
• Angelo Montanari
• Gabriele Puppis

A time granularity can be viewed as the partitioning of a temporal domain in groups of elements, where each group is perceived as an indivisible unit. In this paper we explore an automaton-based approach to the management of time granularity that compactly represents time granularities as single-string automata with counters, that is, Buchi automata, extended with counters, that accept a single infinite word. We focus our attention on the equivalence problem for the class of restricted labeled single-string automata (RLA for short). The equivalence problem for RLA is the problem of establishing whether two given RLA represent the same time granularity. The main contribution of the paper is the reduction of the (non-)equivalence problem for RLA to the satisfiability problem for linear diophantine equations with bounds on variables. Since the latter problem has been shown to be NP-complete, we have that the RLA equivalence problem is in co-NP.

TCS Journal 2004 Journal Article

Phase semantics and decidability of elementary affine logic

• Ugo Dal Lago
• Simone Martini

Light, elementary and soft linear logics are formal systems derived from Linear Logic, enjoying remarkable normalization properties. In this paper, we prove decidability of Elementary Affine Logic, EAL. The result is obtained by semantical means, first defining a class of phase models for EAL and then proving soundness and (strong) completeness, following Okada's technique. Phase models for Light Affine Logic and Soft Linear Logic are also defined and shown complete.

AAAI Conference 2002 Conference Paper

Planning with a Language for Extended Goals

• Ugo Dal Lago
• and Paolo Traverso

Planning for extended goals in non-deterministic domains is one of the most significant and challenging planning problems. In spite of the recent results in this field, no work has proposed a language designed specifically for planning. As a consequence, it is still impossible to specify and plan for several classes of goals that are typical of real world applications, like for instance “try to achieve a goal whenever possible”, or “if you fail to achieve a goal, recover by trying to achieve something else”. We propose a new goal language that allows for capturing the intended meaning of these goals. We give a semantics to this language that is radically different from the usual semantics for extended goals, e. g. , the semantics for LTL or CTL. Finally, we implement an algorithm for planning for extended goals expressed in this language, and experiment with it on a parametric domain.