\n

**Due to the Coronavi
rus outbreak, the workhop is cancelled!**

Around thirty years after the fa ll of Hilbert's program, the proofs-as-programs pa radigm established the view that proofs should con sist in computational or epistemic objects conveyi ng evidence to mathematical propositions. The rela tionship between formal derivations and proofs sho uld then be analogous to the one between words and their meanings. This view naturally gives rise to questions such as 'which conditions should a form al arrangement of symbols satisfy to represent a p roof?' or 'when do two formal derivations represen t the same proof?'. These questions underlie past and current research in proof theory both in the t heoretical computer science community (e.g. catego rical logic, domain theory, linear logic) and in t he philosophy community (e.g. proof-theoretic sema ntics).

\n\nIn spite of these common motiv ations and historical roots, it seems that today p roof theorists in philosophy and in computer scien ce are losing sight of each other. This workshop a ims at contributing to a renaissance of the intera ction between researchers with different backgroun ds by establishing a constructive environment for exchanging views, problems and results.

\n\n < p>In addition to regular invited talks, the worksh op includes two tutorials, aimed at introducing re cent ideas on the correspondence between proofs, p rograms and categories as well as to the historica l and philosophical aspects of the notions of infi nity and predicativity.\n

URL:http://ls.informatik.uni-tuebingen.de/PCM/
CONTACT:Luca Tranchini at luca.tranchini at gmail.
com
CONTACT:Paolo Pistone at paolo.pistone at uniroma3
.it
END:VEVENT
END:VCALENDAR
We in
vite submissions for contributed talks on topics r
elated to the themes of the meeting. These include
, but are not restricted to:

\n - Identi
ty of proofs

\n - Graphical/diagrammati
c representations of proofs

\n - Typed v
s untyped proof theory

\n - Paradoxes an
d circular reasoning

\n - Constructivism
and (im)predicativity

\n - Duality proo
fs/refutations

\n - Computational interp
retations of classical and non-classical logics

\n - Non-deterministic/probabilistic aspec
ts of computation

\n - Inductive/co-indu
ctive constructions in proof theory and type theor
y

\n - (Higher-)categorical proof theory

\n - Substructural aspects of logic

\n - Philosophical and historical reflectio
ns on any of the above