The workshop Proofs, Computation and Meaning is organized by Paolo Pistone and Luca Tranchini and it is funded by the DFG as part of the project Fasilty and refutation. On the negative side of logic (TR1112/4-1).
Scope
Around thirty years after the fall of Hilbert's program, the proofs-as-programs paradigm established the view that a proof should not be identified, as in Hilbert's metamathematics, with a string of symbols in some formal system. Rather, proofs should consist in computational or epistemic objects conveying evidence to mathematical propositions. The relationship between formal derivations and proofs should then be analogous to the one between words and their meanings.
This view naturally gives rise to questions such as “which conditions should a formal arrangement of symbols satisfy to represent a proof?” or “when do two formal derivations represent the same proof?". These questions underlie past and current research in proof theory both in the theoretical computer science community (e.g. categorical logic, domain theory, linear logic) and in the philosophy community (e.g. proof-theoretic semantics).
In spite of these common motivations and historical roots, it seems that today proof theorists in philosophy and in computer science are losing sight of each other. This workshop aims at contributing to a renaissance of the interaction between researchers with different backgrounds by establishing a constructive environment for exchanging views, problems and results.
Important Dates
- Extended abstract submission deadline: 15 January 2020
- Student grant application: 15 January 2020
- Notification: 25 January 2020
- Registration deadline: Extended: 26 February 2020
- Workshop: 20-21 March 2020
- Warm-up for Master and PhD students: 19 March 2020
Invited speakers
- Bahareh Afshari (University of Gothenburg, University of Amsterdam)
- Federico Aschieri (TU Vienna)
- Gilda Ferreira (Universidade Aberta, University of Lisbon)
- Dominic Hughes (UC Berkley)
- Alberto Naibo (Paris 1 University)
- Gabriel Scherer (INRIA, Saclay)
In addition to regular invited talks, the workshop includes two tutorials, aimed at introducing recent ideas on the correspondence between proofs, programs and categories as well as to the historical and philosophical aspects of the notions of infinity and predicativity. Tutorials will be held by:
- Laura Crosilla (University of Oslo)
- Noam Zeilberger (École Polytechnique, Paris)
Contributing speakers
- Matteo Acclavio (INRIA Saclay)
- David Binder (Tübingen Univerisity)
- Patrı́cia Engrácia (Lisbon University)
- Herman Geuvers (Nijmegen \& Eindhoven University)
- Iris van der Giessen (Utrecht University)
- Hidenori Kurokawa (Kanazawa University)
- David Pym (University College London)
- Antonio Piccolomini d'Aragona (Univeristy Aix-Marseille)
- Peter Schuster (University of Verona)
- Lutz Straßburger (INRIA Saclay)
- Daniel Wessel (University of Verona)
Further participants
- Melissa Antonelli (University of Bologna)
- Davide Barbarossa (University of Paris 13)
- Serena Delli (Universidade Nova de Lisboa)
- Boris Eng (University of Paris 13)
- Nico Formanek (HLRS, Stuttgart)
- Marianna Girlando (University of Aix-Marseille)
- Giuseppe Greco (Delft University of Technology)
- Dimitry Ivanov (Hamburg University of Technology)
- Youyou Cong (Tokyo Institute of Technology)
- Elio La Rosa (LMU Munich)
- Matteo Manighetti (INRIA Saclay)
- Andreas Röhler (Independent scholar)
- Nicolas Alexander Schmidt (Humboldt University Berlin)
- Julie Schweer (Karlsruhe Institute of Technology)
- Yuta Takahashi (University of Paris I)