Logic List Mailing Archive

Online Workshop "Proofs, Computation, & Meaning", Virtual, 7 Sep, 28 Sep

7 Dec 2022


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

Third Call For Participation: Online Workshop Series "Proofs, Computation and Meaning"

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

Website: http://ls.informatik.uni-tuebingen.de/pcm-online/

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

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 in a time in which interdisciplinary interactions are made more 
difficult by the pandemic.

The goal is that of creating 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 consists in 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

September 7, 10-13 am (CET)

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.

Program:

10:00-10:30 Hidenori Kurokawa (Kanazawa University): "Takeuti's view of a proof-theoretic analysis of the concept of set"
10-30-10:45 Discussion/Break
10:45-11:15 Gilda Ferreira (Universidade Aberta, University of Lisbon): "The Russell-Prawitz embedding and the atomization of universal instantiation"
11-15-11:30 Discussion/Break
11:30-12:00 Laura Crosilla (University of Oslo): "Cantor's paradise?"
12:00-12:15 Discussion/Break
12:15-12:45 David Binder (Tübingen Univerisity): "Can functional programming be liberated from the natural deduction style? Programming in sequent calculus"
12:45-13:00 Discussion


2. On the syntax of proofs

September 28, 4-7 pm (CET)

Both in natural deduction and in sequent calculs, 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:
- Gabriel Scherer (INRIA Paris-Saclay)
- Bahareh Afshari (University of Gothenburg)
- Herman Geuvers (Nijmegen & Eindhoven University)
- Iris van der Giessen (Utrecht University)
- Matteo Acclavio (Università Roma Tre)


3. On the nature of proofs

December 7, 4-6 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.tranchini@gmail.com 
or paolo.pistone@uniroma3.it.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/

provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam