Partenaires

logo Sphere
CNRS
Logo Université Paris-Diderot Logo Université Paris1-Panthéon-Sorbonne


Rechercher

Sur ce site

Sur le Web du CNRS


Accueil du site > Membres > Pages personnelles > PETROLO Mattia

PETROLO Mattia

JPEG

Doctorant ATER - Université Paris Diderot - Paris 7, Laboratoire SPHERE, Equipe REHSEIS
Me contacter
Me trouver : bureau 476A




- Cursus
- Thèmes de recherche - Équipes
- Publications
- Communications
- Organisation de séminaires et colloques
- Enseignement
- Descriptif de la thèse





Cursus


- 2009 - Début de la cotutelle internationale de thèse avec l’Université Roma Tre - GLGC, avec le soutien de l’Institut des écoles doctorales (bourse « Aides à la mobilité 2010 »)
- 2008 - Rattachement à la Chaire d’Excellence ANR Ideals of Proof
- 2007 - Début de la thèse de doctorat sous la direction de Jean-Baptiste Joinet
- 2007 - Études de Logique Mathématique à l’Université de Paris 7
- 2006 - Laurea Specialistica (niveau M2) en Épistémologie et Logique, Université de Rome "La Sapienza"
- 2003 - Laurea (niveau L3) en Philosophie, Université de Rome "La Sapienza"



Thèmes de recherche - Équipes


- Théorie logique des fondements de l’informatique

  • Logique Mathématique (Théorie de la démonstration, Correspondance de Curry-Howard, Interprétations calculatoires de la logique classique, Logique Linéaire)
  • Philosophie des fondements de l’informatique, Philosophie de la logique, Philosophie des mathématiques
  • Histoire de la logique et des fondements des mathématiques du XXème siècle

- Équipes de recherche (hors SPHERE-REHSEIS)

  • Groupe de logique Roma Tre (GLGC)
  • Ideals of Proof (IP)
  • Théories contemporaines de la logique et philosophie du langage (TCLPL)
  • Projet Vérité et Preuves (VP)



Publications


- Negative translations and duality : toward a unified approach, in A. Lecomte and S. Tronçon (Eds.) : Games, dialogues and interactions, Coll. Folli / LNCS, pp. 188–204, Springer-Verlag Berlin 2011.


En préparation

- Logical Constants from a Computational Point of View : Towards an untyped setting (avec Alberto Naibo et Thomas Seiller), manuscrit communiqué par les auteurs dans des cadres institutionnels divers (Slides).



Communications


Communications programmées

  • Towards a verifcationist account of classical logic, Workshop On Negation, ENS Paris, 12 décembre 2011 (travail en collaboration avec Alberto Naibo).


Communications récentes

- Logique mathématique

  • Logical Constants from a Computational Point of View : Towards an Untyped Setting (avec Thomas Seiller), séminaire du projet ANR LOCI, Centre international de recherches en mathématiques-CIRM, Marseille, 21 janvier 2011.

- Philosophie

  • A computational analysis of logical constants : From inferentialism to an untyped perspective, exposé accepté au Workshop on Logical Constants, ESSLLI 2011, Ljubljana 8-12 août 2011 (travail en collaboration avec Alberto Naibo et Thomas Seiller).
PDF - 327 ko



Organisation de séminaires et colloques


- Co-organisation du symposium « The Meaning of Axioms : From Mathematics to Logic », accepté au 14th Congress of Logic, Methodology and Philosophy of Science, Nancy 19-26 Juillet 2011.

- Co-organisation du réseau de recherche doctoral « Vérité et Preuves ». Co-organisation du colloque final du projet, Université Paris Diderot - Paris 7 et Université Paris 1 - Panthéon-Sorbonne, 21 et 22 Octobre 2011 (Programme).

- Co-organisation de la journée « Proof-theoretic semantics and the justification of logical laws », dans le cadre du séminaire de philosophie des mathématiques – Paris Diderot, 3 mai 2011.

- Organisation (avec Francesca Poggiolesi - Vrije Universiteit Brussel) de la journée d’études « Proofs and Meaning : Logical and Philosophical Perspectives », 22 Mars 2010, Maison des Sciences de l’Homme, Paris, organisée dans le cadre du programme ANR-DFG Hypothetical Reasoning (HYPO).

- Organisation (avec Alberto Naibo - Université Paris 1 Panthéon-Sorbonne) de la journée d’études « New Perspectives on Classical Logic and Axiomatics », Université Paris 1 Panthéon-Sorbonne / Université Paris Diderot - Paris 7, Mardi 16 Juin 2009.



Enseignement


2010-2011 : Cours/TD Logique L1, Université Paris 1 – Panthéon Sorbonne.



Descriptif de la thèse


Les métamorphoses de la « constructivité logique » : une analyse épistémologique de la constructivisation de la logique classique

Dans mon travail de thèse je me propose dans un premier temps d’analyser les différents discours sur la constructivité logique élaborés au fil de l’histoire de la logique. Dans un deuxième temps, je souhaite examiner plus précisément les débats concernant la question de la constructivité / non constructivité de la logique classique. Mon point de départ est un constat d’ordre historique : jusqu’à la fin des années quatre-vingt dix, la logique classique était consensuellement considérée comme non-constructive. Aujourd’hui, dans le cadre de cette branche de la logique qu’on appelle la « théorie de la démonstration », elle est au contraire unanimement considérée comme constructive.

À partir de la « découverte » de l’isomorphisme de Curry-Howard (correspondance preuves-programmes, 1969), le concept de constructivité s’est nettement et profondément transformé. Cet isomorphisme fournit, en effet, une base technique solide pour l’étude de la nature calculatoire de la logique intuitionniste. Pendant une longue période, les obstacles qui semblaient s’opposer à une extension de la correspondance preuves-programmes au cas de la logique classique, constituèrent autant d’explications du fait que la logique classique n’était pas, par nature, constructive.

Plusieurs types de solutions techniques à ce problème ont été depuis lors proposés. Aujourd’hui, dans ce contexte, la question de la « constructivisation » de la logique classique est devenue celle de savoir s’il est possible de la formaliser comme système calculatoire doué de « bonnes » propriétés calculatoires. C’est donc de ce côté là qu’il s’agira pour moi de chercher les critères nouveaux de la constructivté. A l’heure actuelle, il n’existe pas à ma connaissance de travail systématique de comparaison et d’évaluation théorique de ces travaux visant la constructivisation de la logique classique. Le second objectif de ma thèse consistera précisément à combler cette lacune.