paolo.pistone[at]uniroma3.it

paolo.pistone2[at]unibo.it

Università di Bologna,

Dipartimento di Informatica - Scienze e Ingegneria

v. Mura Anteo Zamboni 7, 40126, Bologna, Italy.

I am a post-doc researcher in logic, currently working within Ugo Dal Lago's ERC CoG project DIAPASoN at the University of Bologna.

I obtained my joint PhD in Mathematics and Philosophy in 2015 from Aix-Marseille University and the University of 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

*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 (2021), https://doi.org/10.1007/s11225-021-09964-z, ArXiv;*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;*On Counting Propositional Logic*(with Melissa Antonelli and Ugo Dal Lago), ArXiv;*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.

*A New Conjecture About Identity of Proofs*, ArXiv;-
*Intensional harmony as isomorphism*(with Luca Tranchini),

to appear in Thomas Piecha and Kai Wehmeier (eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics, Outstanding Contributions to Logic, Springer; -
*On paradoxes in normal form*(with Mattia Petrolo),

TOPOI [Special Issue Inferences and Proof], 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.

*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.

*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.

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

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

*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).