From Hypersequents to Parallel Processes

Francesco Genco (TU Wien)

Francesco Genco (TU Wien) will present "From Hypersequents to Parallel Processes" on Feb 24 at 11 in Old Quad G09. 

Abstract: The system of rules formalism combines ideas from natural deduction and sequent calculus achieving a great expressive power. Focusing on propositional intermediate logics, we prove that a rather simple restriction of such formalism (two-level systems of rules) is equivalent to the hypersequent formalism. This result has several proof-theoretical consequences and, furthermore, provides a strong connection between hypersequent calculi and natural deduction. Exploiting such connection we define a Curry--Howard correspondence for Gel logic, and prove that the resulting system enjoys normalisation and the subformula property. The lambda calculus obtained features constructs representing higher-order communication between parallel processes, and its reduction rules admit a meaningful computational interpretation in terms of code optimisation by code mobility.