Paolo Pistone
paolo.pistone[at]ens-lyon.fr
paolo.pistone[at]uniroma3.it
Junior Professor (Chaire Professeur Junior) at Université Claude Bernard Lyon 1 and
Laboratoire de l'Informatique du Parallélisme.
Address: École Normale Supérieure de Lyon, 46 allée d'Italie, 69007 Lyon.
Previously I was:
- Assistant Professor at Dipartimento di Informatica - Scienza e Ingegneria, Università di Bologna (2023),
- 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 Curry-Howard Correspondence (CHC) between formal proofs and verified functional programs or, 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 to account for approximated and probabilistic programs.
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
PhD students
Amélie Rima (Inria Saclay/ENS Lyon)
Guido Fiorillo (UCBL)
Papers and pre-prints:
Mathematical Logic/ Theoretical Computer Science:
-
The Lambda Calculus is Quantifiable (with Valentin Maestracci).
To appear in Proceedings CSL 2025.
-
Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs (with Davide Barbarossa),
Extended Version.
Proceedings CSL 2024, LIPIcs vol. 288, pp. 14:1-14:23, 2024;
-
Enumerating Error-Bounded Polytime Algorithms Through Arithmetical Theories (with Melissa Antonelli, Ugo Dal Lago, Davide Davoli, and Isabel Oitavem),
Extended Version.
Proceedings CSL 2024, LIPIcs vol. 288, pp. 10:1-10:19, 2024;
-
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, vol. 175, Issue 9, 2024;
-
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,
ArXiv
A. Piccolomini d'Aragona (ed.), Perspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction, Synthèse Library, Springer, 2024;
-
Intensional harmony as isomorphism (with Luca Tranchini),
T. Piecha and K. Wehmeier (eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics, Outstanding Contributions to Logic, Springer, 2024;
-
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ávicka, 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.
Outreach: