Martedì 22/10/13, ore 18, Dipartimento di Matematica e Fisica, Aula Seminari 311, largo San L. Murialdo 1 - Roma, Emanuel Beffara (IML - Aix-Marseille Université) terrà un seminario dal titolo Interaction in proof theory: from classical realizability to concurrency , promosso dal Gruppo di Ricerca in “Logica e Geometria della Cognizione” presso il Dipartimento di Matematica e Fisica.

Abstract
Classical realizability is a technique for extracting computational content
from classical proofs. It was introduced by Krivine in the middle of the
1990's combining ideas from traditional Kleene realizability and from logical
translations from classical to intuitionistic logics. Its fundamental
contribution is to put the notion of interaction (between a proof and a
counter-proof, or between a program and its environment) in a central position
explicitly. Subsequently, it provides enlightening descriptions of the
computational behaviour of classical tautologies as synchronization mechanisms
between threads of a program.

In this talk, I will survey the fundamental ideas that lead to the
interactive study of proofs with the tools of classical realizability,
in the original framework of the ?-calculus with control operators. I
will show how these ideas relate to other models for proof systems
(games, ludics…), how it can be extended to other models of computation
and what it can teach us about the ongoing question of the proof-program
correspondence for concurrent computation.

Per informazioni:
L.Tortora de Falco,
tel. 0657338415, tortora@uniroma3.it
http://logica.uniroma3.it