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

\nAbstract: 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.

ORGANIZER;CN=Shawn Standefer: METHOD:PUBLISH END:VEVENT END:VCALENDAR