Paolo Pistone

paolo.pistone2[at]unibo.it
paolo.pistone[at]uniroma3.it

Assistant Professor at Dipartimento di Informatica - Scienza e Ingegneria,
Università di Bologna, Mura Anteo Zamboni 7, Bologna, Italy.

Previously I was:

Assistant Professor at Dipartimento di Matematica e Fisica, Università Roma Tre (2022-2023),
post-doc at Dipartimento di Informatica-Scienza e Ingegneria, Università di Bologna, within Ugo Dal Lago's ERC project DIAPASoN (2019-2022),
post-doc at the Wilhelm Schickard Institute for Computer Science at Tübingen University (2018-2019),
post-doc at Dipartimento di Matematica e Fisica,
Università Roma Tre (2016-2018),
ATER at the Institut de Mathématiques de Marseille, Université d'Aix-Marseille (2015-2016).

I obtained a joint PhD in Mathematics and Philosophy in 2015 from Université d'Aix-Marseille and Università Roma Tre, under the supervision of Jean-Yves Girard and Michele Abrusci. My PhD thesis (that you can find below) was awarded the "Prix de Thèse 2016" by Aix-Marseille University.
Here is my CV (last update: April 2022).

My research interests are in logic and in the semantics of programming languages, and revolve around the good old Curry-Howard Correspondence (CHC) between formal proofs and verified functional programs (more precisely, between proof systems and typed lambda-calculi). In particular, much of my research has been devoted to System F, a cornerstone of the CHC relating (impredicative) second order quantification in logic with polymorphic programming. More recently, I have been investigating extensions of the CHC correspondence to account for programs whose verification is intrinsically approximated or probabilistic.

Key words:

second order logic / System F: proof-theory, categorical semantics, parametricity, impredicativity
general proof theory: identity of proofs/program equivalence, linear logic, proof nets
differential semantics: program similarity/metrics, logics for probabilistic programs

Papers and pre-prints:

Mathematical Logic/ Theoretical Computer Science:

Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs (with Davide Barbarossa), available soon.
To appear in CSL 2024 Proceedings;
Enumerating Error-Bounded Polytime Algorithms Through Arithmetical Theories (with Melissa Antonelli, Ugo Dal Lago, Davide Davoli, and Isabel Oitavem), available soon.
To appear in CSL 2024 Proceedings;
Differences and Metrics in Program Semantics: Advances in Quantitative Relational Reasoning (volume edited with Ugo Dal Lago and Francesco Gavazzo),
Mathematical Structures in Computer Science, Special Issue 4-5, Vol. 33, 2023;
Towards Logical Foundations for Probabilistic Computation (with Melissa Antonelli and Ugo Dal Lago),
Annals of Pure and Applied Logic, in press, 2023;
On Counting Propositional Logic and Wagner's Hierarchy (with Melissa Antonelli and Ugo Dal Lago),
Theoretical Computer Science, Vol. 966-967, 2023;
On the Lattice of Program Metrics (with Ugo Dal Lago and Naohiko Hoshino),
Proceedings FSCD 2023, LIPIcs vol. 260, pp. 20:1-20:19, 2023;
Curry and Howard Meet Borel (with Melissa Antonelli and Ugo Dal Lago), Extended Version
Proceedings LICS 2022, IEEE Computer Society, pp. 1-13, 2022;
On Quantitative Algebraic Higher-Order Theories (with Ugo Dal Lago, Furio Honsell and Marina Lenisa), Extended Version
Proceedings FSCD 2022, LIPIcs vol. 228, pp. 4:1-4:18, 2022;
From Identity to Difference: A Quantitative Interpretation of the Identity Type, ArXiv;
The naturality of natural deduction II. On atomic polymorphism and generalized propositional connectives (with Luca Tranchini and Mattia Petrolo),
Studia Logica, vol. 110, pp. 545-592, 2022;
The Yoneda Reduction of Polymorphic Types (Abstract) (with Luca Tranchini),
Proceedings SOQE 2021, CEUR Workshop Proceedings, pp. 92-97, 2021;
On Counting Propositional Logic and Wagner's Counting Hierarchy (with Melissa Antonelli and Ugo Dal Lago),
Proceedings ICTCS 2021, CEUR Workshop Proceedings, pp. 107-121, 2021;
On Generalized Metric Spaces for the Simply Typed Lambda-Calculus,
Proceedings LICS 2021, IEEE Computer Society, pp. 1-14, 2021 (online talk);
What's Decidable about (Atomic) Polymorphism? (with Luca Tranchini),
Proceedings FSCD 2021, LIPIcs vol. 195, pp. 27:1-27:23, 2021 (online talk);
On Measure Quantifiers in First-Order Arithmetic (with Melissa Antonelli and Ugo Dal Lago),
Proceedings CiE 2021, LNCS vol. 12813, pp. 12-24, 2021;
A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations (with Guillaume Geoffroy),
Proceedings CSL 2021, LIPIcs vol. 183, pp. 23:1-23:18, 2021;
The Yoneda Reduction of Polymorphic Types (with Luca Tranchini), Extended Version,
Proceedings CSL 2021, LIPIcs vol. 183, pp. 35:1-35:22, 2021 (online talk from minute 53:23);
Finite semantics of polymorphism, complexity and the power of type fixpoints (with L.T.D. Nguyễn, T. Seiller and L. Tortora de Falco);
Proof nets, coends and the Yoneda isomorphism,
Proceedings Linearity-TLLA 2018, ArXiv :1904.06159; EPTCS 292, pp. 148-167, 2019;
Proof nets and the instantiation overflow property, ArXiv;
On completeness and parametricity in the realizability semantics of System F,
Logical Methods in Computer Science, 15(4), pp. 6:1-6:54, 2019;
Polymorphism and the obstinate circularity of second order logic: a victims' tale,
The Bulletin of Symbolic Logic, 24(1), pp. 1-52, 2018. Link to BSL;
The naturality of natural deduction I (with Luca Tranchini and Mattia Petrolo)
Studia Logica, 107(1), pp. 195-231, 2019. Link to SL;
On dinaturality, typability and beta-eta-stable models,
Proceedings FSCD 2017, LIPIcs vol. 84, pp. 29:1--29:17, 2017;
Logic Programming and Logarithmic Space (with C. Aubert, M. Bagnol and T. Seiller),
Programming Languages and Systems, 12th Asian Symposium APLAS 2014, Singapore, volume 8858 of Lecture Notes in Computer Science, pp. 39-57, Springer, 2014.

Philosophy of Logic:

A New Conjecture About Identity of Proofs,
to appear in A. Piccolomini d'Aragona (ed.), Perspectives on Deduction, Synthèse Series;
Intensional harmony as isomorphism (with Luca Tranchini),
to appear in T. Piecha and K. Wehmeier (eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics, Outstanding Contributions to Logic, Springer;
On paradoxes in normal form (with Mattia Petrolo),
Topoi, 38(3), pp. 605-617, 2019;
A normal paradox (with Mattia Petrolo),
In Arazim, P. and Lávička, T., editors, The Logica Yearbook 2016, p. 173-184. College Publications, London, 2017;
On the "no-deadlock criterion": from Herbrand's theorem to Geometry of Interaction,
New Developments in Logic and Philosophy of Science, SILFS series, College Publications, 2016;
Rule-following and the limits of formalization: Wittgenstein's considerations through the lens of logic, preprint,
From Logic to Practice, Italian Studies in the Philosophy of Mathematics, volume 308 of Boston Studies in the Philosophy and History of Science, Springer, 2015;
On transcendental syntax: a Kantian program for logic? (with V.M. Abrusci), preprint,
Second Pisa Colloquium in Logic, Epistemology and Philosophy of Language, ETS, Pisa, 2014;
Dalle regole dell'argomentazione alla logica delle regole.
Rivista Italiana di Filosofia Analitica Junior, vol. 1 n. 2, pp. 25-38, 2010.

Other stuff:

On proofs and types in second order logic, my PhD thesis, PDF;
Le direzioni della ricerca logica in Italia: la logica lineare e i suoi sviluppi (with V.M. Abrusci),
in Hykel Hosni, Gabriele Lolli, Carlo Toffalori, editors, Le direzioni della ricerca logica in Italia 2, p. 1-47, Edizioni ETS, Pisa, 2018;
L'Hotel di Hilbert e l'imbarazzo della scelta (with Fabio Pasquali),
Archimede, vol. 1/2017, Le Monnier, 2017;
La geometria dell'interazione, un paradigma monista per la logica, PDF.

Recent talks:

The calculus of higher level rules in modern dress, Third Proof-Theoretic Semantics Conference, Uni-Tübingen, March 29, 2019;
Some results on program equivalence in second order linear logic, PPS seminar, IRIF, Paris 7, March 21, 2019;
Coends and proof equivalence in second order multiplicative linear logic, Chocola seminar, LIP, ENS Lyon, December 13, 2018;
Syntactic dinaturality and proof equivalence in System F and second order linear logic , Parsifal seminar, LIX, Palaiseau, November 21, 2018;
Relating the realizability and parametricity interpretations of System F, Seminar of the LIMD team, Université de Savoie, Chambéry, November 8, 2018;
Identity of proofs and second order types, workshop "Le mème et l'autre : identité, orthogonalité et types", Lyon 3, November 5, 2018;
Proof equivalence in second order multiplicative linear logic, Joint GDRI-Crecogi-Elica workshop, IRIF, Paris 7, October 9, 2018;
Instantiation overflow, from the viewpoint of categorical semantics and linear logic, Logic seminar, Lisbon University, September 17, 2018;
Coends and proof equivalence in second order multiplicative linear logic, Logic and Verification team seminar, LIPN, Paris 13, June 8, 2018.

Teachings@UniTübingen:

Introduction to denotational semantics, Wintersemester 2018-2019
From denotational semantics to linear logic, Sommersemester 2018-2019

Teachings@UniRomaTre:

Modelli di calcolo (IN410), tutorials (2017-2018)
Logica e comunicazione, tutorials (2017-2018)
Modelli di calcolo (IN410), tutorials (2016-2017)

Outreach:

La Tournée de π, http://www.piday.fr/;
The European Researcherers Night at Università Roma Tre, http://nottericerca.uniroma3.it/, The (L)imitation game (slides);
Treizes Minutes Jeunes Chercheurs 2016, Aristote et le branchement des idées (video, slides).