<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>