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

[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.tranchini at gmail.com or
paolo.pistone at uniroma3.it.

Participants will receive a link a few days before each event.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220921/46da8087/attachment-0001.htm>