Fwd: [CfPart / Reminder] Proofs, computation and meaning II (28 September, online)

[Joao Marcos]

---------- Forwarded message ---------

From: Luca Tranchini
Call For Participation: Online Workshop Series "Proofs, Computation and Meaning"

Online events: September 7, September 28 and December 7, 2022

*******************************************************************************

This online workshop series was originally planned as an in person
meeting which was canceled due to the outbreak of the Coronavirus
pandemic in early March 2020.

The event was planned to bring researchers whose work focuses on the
notion of formal proof from either a philosophical, computational or
mathematical perspective. With the obvious limitations of an online
format, we wish to keep this original motivation, which looks even
more timely now that interdisciplinary interactions are made more
difficult by the pandemic.

The goal is to create an opportunity for members of different
communities to interact and exchange their views on proofs, their
identity conditions, and the more convenient ways of representing them
formally.

*******************************************************************************

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.

*******************************************************************************

ORGANIZATION:

The workshop series includes three events, each focusing on one
specific aspect of proofs and their representation. To foster
interaction and discussion, each event will consist of short talks
followed by a 15 minutes slot during which participants can engage in
discussion or just take a short break.


1. Infinity and co-inductive proofs [held on September 7, 10 am (CEST)]

In Hilbert's program, the role of proof theory was that of assuring a
solid finitistic foundations for the use of infinitary concepts in
mathematics. By contrast, and somehow paradoxically, the development
of the discipline led to the study of proof systems explicitly
incorporating infinitary ideas such as impredicativity, co-induction
and other constructions.

Speakers:
- David Binder (Tübingen University)
- Laura Crosilla (University of Oslo)
- Gilda Ferreira (Universidade Aberta & University of Lisbon)
- Hidenori Kurokawa (Kanazawa University)


2. On the syntax of proofs [September 28, 4-7 pm (CEST)]

Both in natural deduction and in sequent calculus, as well as in their
associated type systems, the rules of the standard connectives have
been generalized in various ways, thereby obtaining proof-theoretic
characterizations of various families of connectives or more generally
of data type constructors. Although the motivations for such
generalizations are apparently very different (ranging from
considerations about the inherent duality of the calculi, to the
relation between syntax and semantics, to questions arising in the
study of proof-search strategies), they often have a lot in common.

Speakers:
- Matteo Acclavio (INRIA Paris-Saclay)
- Bahareh Afshari (University of Gothenburg)
- Herman Geuvers (Nijmegen & Eindhoven University)
- Iris van der Giessen (Utrecht University)
- Gabriel Scherer (INRIA Paris-Saclay)


3. On the nature of proofs [December 7, 4 pm (CET)]

The developments of logic, and of proof theory in particular, have
lead us to look at proofs primarily through the lens of various formal
systems, such as natural deduction, sequent calculus, tableaux, proof
nets etc. Yet, is it possible to investigate the nature of proofs,
their identity conditions, their relations with computation and with
meaning in a direct way, i.e. independently of the choice of a
particular formal system?

Speakers:
- Noam Zeilberger (INRIA Paris-Saclay)
- Alberto Naibo (Paris 1 University)
- Antonio Piccolomini d'Aragona (Aix-Marseille University)


*******************************************************************************

CALL FOR PARTICIPATION:

If you wish to attend, please send an e-mail to
luca.tr...@gmail.com or paolo....@uniroma3.it.

Participants will receive a link a few days before each event.