Cari tutti,
il prossimo seminario del gruppo di ricerca in “Logica e Geometria della Cognizione” avrà luogo questo venerdì presso il dipartimento di Matematica e Fisica, l.go S.Leonardo Murialdo 1, alle ore 11 in aula 311 (edificio C, terzo piano).

Virgile Mogbil, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13
Proofs as schedules

Abstract:
« Proofs as schedules » is a new approach about the proof-theoretic study of concurrent interaction. Through the Curry-Howard correspondence proof theory is well suited to describe confluent systems. Because the meaning of proofs lies in their normal forms, cut elimination should be confluent in order to preserve it. On the other hand concurrency has non-determinism as a fundamental feature. In process calculi the meaning of a term is not its final irreducible form but what happens to get there, as interaction with other processes... hence term reduction i.e. execution of interactions should definitely not preserve meaning. We propose a correspondence between proofs in linear logic and interaction plans for processes, called schedules.