Paolo Pistone
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 postdoc 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 AixMarseille University and the University of Roma Tre, under the supervision of JeanYves Girard and Michele Abrusci. My PhD thesis (that you can find below) was awarded the "Prix de Thèse 2016" by AixMarseille University.
Here is my CV.
My research interests are in the prooftheory of second order logic (System F) and linear logic (especially proofnets).
Parametric polymorphism, the central topic of second order prooftheory, lies at the border between mathematics,
computer science, and
philosophy. It can be considered as the mathematical counterpart of the old philosophical problem of impredicativity. Also, polymorphism is a wellknown tool of many programming languages and has deep connections with category theory
(dinaturality, coherence theorems, fibrations).
Papers and preprints:
Mathematical Logic:
 The naturality of natural deduction II. Remarks on atomic polymorphism (with Luca Tranchini and Mattia Petrolo), ArXiv;
 Polymorphism and the free bicartesian closed category (with Luca Tranchini), ArXiv;
 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 LinearityTLLA 2018, arXiv :1904.06159 ; EPTCS 292, 2019, pp. 148167;
 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:16:54, 2019;
 Polymorphism and the obstinate circularity of second order logic: a victims' tale,
The Bulletin of Symbolic Logic, 24(1), pp. 152, 2018. Link to BSL;
 The naturality of natural deduction I (with Luca Tranchini and Mattia Petrolo)
Studia Logica, 107(1), pp. 195231, 2019. Link to SL;
 On dinaturality, typability and betaetastable models,
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics (LIPIcs), vol. 84, pp. 29:129:17, Schloss DagstuhlLeibnizZentrum fuer Informatik, Dagstuhl, Germany, 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. 3957, Springer, 2014.
Philosophy of Logic:

On paradoxes in normal form (with Mattia Petrolo),
TOPOI [Special Issue Inferences and Proof], 38(3), pp. 605617, 2019;
 A normal paradox (with Mattia Petrolo),
In Arazim, P. and Lávička, T., editors, The Logica Yearbook 2016, p. 173184. College Publications, London, 2017;
 On the "nodeadlock criterion": from Herbrand's theorem to Geometry of Interaction,
New Developments in Logic and Philosophy of Science, SILFS series, College Publications, 2016;
 Rulefollowing 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. 2538, 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. 147, 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 ProofTheoretic Semantics Conference, UniTü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 GDRICrecogiElica 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:
Teachings@UniRomaTre:
Outreach: