6 citations · 14 across the 19 of their papers we have counts for
28 papers
On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic
Ugo Dal Lago, Guido Fiorillo, Paolo Pistone
The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually -complete. For this reason, a gr…
On the Metric Nature of (Differential) Logical Relations
Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone
Differential logical relations are methods to measure distances between higher-order programs where distances between functional programs are themselves \emph{functions}, relating…
Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction
Kostia Chardonnet, Ugo Dal Lago, Naohiko Hoshino +1
We present an algorithm turning any term of a linear quantum -calculus into a quantum circuit. The essential ingredient behind the proposed algorithm is Girard's geometry of int…
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 betwe…
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
Davide Barbarossa, Paolo Pistone
In the last few years there has been a growing interest towards methods for statistical inference and learning based on computational geometry and, notably, tropical geometry, that…
The Lambda Calculus is Quantifiable
Valentin Maestracci, Paolo Pistone
In this paper we introduce several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to me…
On Randomized Computational Models and Complexity Classes: a Historical Overview
Melissa Antonelli, Ugo Dal Lago, Paolo Pistone
Since their appearance in the 1950s, computational models capable of performing probabilistic choices have received wide attention and are nowadays pervasive in almost every areas…
Tropical Mathematics and the Lambda Calculus I: Metric and Differential Analysis of Effectful Programs
Davide Barbarossa, Paolo Pistone
We study the interpretation of the lambda-calculus in a framework based on tropical mathematics, and we show that it provides a unifying framework for two well-developed quantitati…
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
Melissa Antonelli, Ugo Dal Lago, Davide Davoli +2
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)…
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…
On Quantitative Algebraic Higher-Order Theories
Ugo Dal Lago, Furio Honsell, Marina Lenisa +1
We explore the possibility of extending Mardare et al. quantitative algebras to the structures which naturally emerge from Combinatory Logic and the lambda-calculus. First of all,…
Curry and Howard Meet Borel
Melissa Antonelli, Ugo Dal Lago, Paolo Pistone
We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambd…
A New Conjecture About Identity of Proofs
Paolo Pistone
A central problem in proof-theory is that of finding criteria for identity of proofs, that is, for when two distinct formal derivations can be taken as denoting the same logical ar…
From Identity to Difference: A Quantitative Interpretation of the Identity Type
Paolo Pistone
We explore a quantitative interpretation of 2-dimensional intuitionistic type theory (ITT) in which the identity type is interpreted as a "type of differences". We show that a frag…
What's Decidable about (Atomic) Polymorphism
Paolo Pistone, Luca Tranchini
Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the mos…
On Generalized Metric Spaces for the Simply Typed Lambda-Calculus (Extended Version)
Paolo Pistone
Generalized metrics, arising from Lawvere's view of metric spaces as enriched categories, have been widely applied in denotational semantics as a way to measure to which extent two…
On Measure Quantifiers in First-Order Arithmetic (Long Version)
Melissa Antonelli, Ugo Dal Lago, Paolo Pistone
We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the…
On Counting Propositional Logic
Melissa Antonelli, Ugo Dal Lago, Paolo Pistone
We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly ma…
The naturality of natural deduction (II). Some remarks on atomic polymorphism
Paolo Pistone, Luca Tranchini, Mattia Petrolo
In a previous paper (of which this is a prosecution) we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translat…
The Yoneda Reduction of Polymorphic Types (Extended Version)
Paolo Pistone, Luca Tranchini
In this paper we explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isom…
Around finite second-order coherence spaces
Lê Thành Dũng Nguyên
Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We exhib…
Proof Nets, Coends and the Yoneda Isomorphism
Paolo Pistone
Proof nets provide permutation-independent representations of proofs and are used to investigate coherence problems for monoidal categories. We investigate a coherence problem conc…
Proof nets and the instantiation overflow property
Paolo Pistone
Instantiation overflow is the property of those second order types for which all instances of full comprehension can be deduced from instances of atomic comprehension. In other wor…