7 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 g…
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 in…
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…
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…
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…