"Proofs and types", 25 years later

Gruppo di Logica e Geometria della Cognizione
HYPOTHESES, Hypothetical Reasoning – Its Proof-Theoretic Analysis, joint French-German research project funded by ANR and DFG
Dipartimento di “Filosofia, Comunicazione, Spettacolo", Scuola di "Lettere, Filosofia, Lingue” (ex Facoltà di Lettere e Filosofia), via Ostiense 234.

The publication, twenty-five years ago, of the by now classical textbook "Proofs and Types" (Girard, Lafont, Taylor 1989) marked the consolidation of the tradition arising from the Curry-Howard connection between logic (natural deduction) and theoretical computer science (typed lambda calculi).
Many developments and extensions of this connection have been investigated in the last years (by means of linear logic, abstract machines, geometry of interaction, ludics, just to name some directions of research), providing at the same time several theoretical challenges to the original Curry-Howard paradigm.
Then, some important questions related to logic and philosophy naturally arise, e.g. the following two questions:
1) What has the correspondence between logic and computation evolved into during these years?
2) What was the impact of this tradition on the philosophical investigations on the foundations of logic and mathematics?


Thursday, 26 March, Aula Verra (ground floor)

15 :30-16 :15 Wagner de Campos Sanz (Universidade de Goiás, Brasil)

16 :15-17 :00 Giulio Guerrieri (PPS, Univ. Paris 7)
Injectivity of relational semantics for connected MELL proof-structures via Taylor expansion

17 :00-17 :15 Coffee break

17 :15-18 :00 Jean Fichot (IHPST, Univ. Paris 1)
May Falsum be true?

Friday, 27 March, Aula Verra (ground floor)

9 :00-10 :15 Jean-Yves Girard (I2M, Aix-Marseille Univ.)
La surprenante syntaxe transcendantale du calcul des prédicats

10 :30-13 :30 Defense of Paolo Pistone’s thesis
On proofs and types in second order logic

13 :30-15 :30 Lunch (foyer next to the Aula Magna)

15 :30-16 :15 Pierre-Louis Curien (PPS, Univ. Paris 7)
Curry-Howard correspondence, abstract machines, sequent calculus, and classical logic

16 :15-17 :00 Jean-Baptiste Joinet (Univ. Lyon 3)
On the « primitive » distinction Individual/Predicate

17 :00-17 :15 Coffee break

17 :15- 18 :00 Pierre Livet (Aix-Marseille Univ.)
Epistemic circularity: self-justification versus self-application; meaning as the source of use or computational functioning as the regulation of impredicativity?

Saturday, 28 March, Aula Verra (ground floor)

9 :30-10 :15 Alain Lecomte (Univ. Paris 8)
Ludics and philosophy of language: from literal meaning to dialogue modeling

10 :15-10 :30 Coffee break

10 :30-11 :15 Marco Pedicini (Univ. Roma Tre)
Sequential and parallel abstract machines for optimal reduction

11 :15 -12 :00 Vito Michele Abrusci (Univ. Roma Tre)
Logic, first-order logic, second-order logic in Hilbert’s logical school (1920-1940): some historical remarks