Intermediate logics and concurrent λ-calculi: a proof-theoretical approach

Abstract

Avron speculated in 1991 that the proof-theoretical formalism of hypersequents might be connected with concurrent computation and that it should be possible to use the intermediate logics that can be naturally captured by hypersequent calculi as bases for parallel -calculi. We define parallel and concurrent -calculi based on CurryHoward correspondences for intermediate logics that can be formalized as hypersequent calculi. The introduced calculi are more expressive than simply-typed -calculus and can formalize interesting parallel and concurrent programs. We thus confirm Avrons thesis. In order to do so, we first provide a general translation from hypersequent calculi to suitable natural deduction calculi. We then use the obtained proof systems for classical and GodelDummett logic to define the first concurrent computational interpretations of these well-known logics. The resulting calculi Cl and G are concurrent extensions of simply typed -calculus. We then introduce , a parallel extension of simply typed -calculus. Its type system is based on an infinite set of axioms corresponding to hypersequent rules and can be used to type terms that correspond to generic communication topologies. We prove strong normalization for and showcase its expressive power by programming examples. Since the type system of only corresponds to a fragment of the considered intermediate logics, we also provide a concurrent computational interpretation for the full logical systems. The normalization of the resulting calculi require general communication reductions also featured in Cl and G that ensure that the subformula property holds and implement code mobility techniques for function closure transmission.