<div dir="ltr"><div>Call For Participation: Online Workshop Series "Proofs, Computation and Meaning"</div>
<div><br>
</div>
<div>Online events: September 7, <b>September 28</b> and December 7, 2022</div>
<div><br>
</div>
<div>*******************************************************************************</div>
<div><br>
</div>
<div>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.
</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>*******************************************************************************</div>
<div><br>
</div>
<div>SCOPE:</div>
<div><br>
</div>
<div>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.</div>
<div> </div>
<div>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).</div>
<div> </div>
<div>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.</div>
<div><br>
</div>
<div>*******************************************************************************</div>
<div><br>
</div>
<div>ORGANIZATION:</div>
<div><br>
</div>
<div>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.</div>
<div><br></div><div><br>
</div>
<div>1. Infinity and co-inductive proofs [held on September 7, 10 am (CEST)]</div><div><br></div><div>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. <br></div><div><br></div>Speakers:<br>- David Binder (Tübingen University)<br>- Laura Crosilla (University of Oslo)<br>- Gilda Ferreira (Universidade Aberta & University of Lisbon)<br>- Hidenori Kurokawa (Kanazawa University)<br><br><br><b>2. On the syntax of proofs [September 28, 4-7 pm (CEST)</b>]
<div><br></div>
<div>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.</div>
<div><br>
</div>
<div>Speakers:</div><div><div>- Matteo Acclavio (INRIA Paris-Saclay)</div>
</div>
<div><div>- Bahareh Afshari (University of Gothenburg)</div>
<div>- Herman Geuvers (Nijmegen & Eindhoven University)
<div></div></div></div><div>- Iris van der Giessen (Utrecht University)<div>- Gabriel Scherer (INRIA Paris-Saclay)</div></div><div><br></div><div><br></div><div>3. On the nature of proofs [December 7, 4 pm (CET)]</div>
<div><br>
</div>
<div>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?</div>
<div><br>
</div>
<div>Speakers:</div>
<div>- Noam Zeilberger (INRIA Paris-Saclay)</div>
<div>- Alberto Naibo (Paris 1 University)</div>
<div>- Antonio Piccolomini d'Aragona (Aix-Marseille University)</div>
<div><br>
</div>
<div><br>
</div>
<div>*******************************************************************************</div>
<div><br>
</div>
<div>CALL FOR PARTICIPATION:</div>
<div><br>
</div>
<div>If you wish to attend, please send an e-mail to <a href="mailto:luca.tranchini@gmail.com" target="_blank">luca.tranchini@gmail.com</a> or <a href="mailto:paolo.pistone@uniroma3.it" target="_blank">paolo.pistone@uniroma3.it</a>.</div>
<div><br>
</div>
<div>Participants will receive a link a few days before each event.</div>
<div><br>
</div></div>