Due to the Coronavirus outbreak, the workhop is cancelled!

We apologize for any inconvenience this may cause.

 

 

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

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:

 

Contributing speakers

 

Further participants