[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
*Apologies for cross postings*
*******************************************************************************
Second Call For Participation: Online Workshop Series "Proofs, Computation and
Meaning"
Online events: September 7, September 28 and December 7, 2022
Website:
https://urldefense.com/v3/__http://ls.informatik.uni-tuebingen.de/pcm-online/__;!!IBzWLUs!QgWjwYc0PXbtDgc_opPhEQf4y3FAjLEPhrMIY64XNGqh5blugak0SUlKNPg7TdPEWzZp92pbbWvd4XJPN2usOQLcOSX5_fP8gNzxP_b8mg$
*******************************************************************************
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.
Speakers:
- Laura Crosilla (University of Oslo)
- Hidenori Kurokawa (Kanazawa University)
- David Binder (University of Tübingen)
- Gilda Ferreira (Lisbon University)
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 [email protected] or
[email protected].
________________________________
Da: Paolo Pistone
Inviato: lunedì 11 luglio 2022 14:43
Oggetto: Call for Participation: Online Workshop Series "Proofs, Computation
and Meaning"
*Apologies for cross postings*
*******************************************************************************
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 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 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.
Speakers:
- Laura Crosilla (University of Oslo)
- Hidenori Kurokawa (Kanazawa University)
- David Binder (University of Tübingen)
- Gilda Ferreira (Lisbon University)
2. On the syntax of proofs
September 28, 4 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 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 [email protected] or
[email protected].
A link to access the online events will be shared later.
