Virgile Mogbil, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13
Quando:
23/10/2015 - 11:00
Dove:
Dipartimento di Matematica e Fisica, Università Roma Tre
Largo S. Leonardo Murialdo 1, Roma
Palazzina C, III piano, Aula 311
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.
