Affiliations: Dipartimento di Informatica, Universitá degli Studi di Verona, Italy. gianluigi.bellin@univr.it
Note: [] We thank Phil Scott and Tristan Crolard for their cooperation over the years on the topics of this paper. We had useful conversations with Federico Aschieri, Corrado Biasi, Alessandra Carbone, Carlo Dalla Pozza, Giuditta Franco, Hugo Herbelin, Neil Jones, Damiano Macedonio, Vincenzo Manca, Massimo Merro, Michel Parigot, Andy Pitts, Kurt Ranalter, Carolyn Talcott and Graham White. We thank an anonymous referee for helpful suggestions. Address for correspondence: Dipartimento di Informatica - Universitá degli Studi di Verona, Strada Le Grazie 15, 37134 Verona, Italy
Note: [] We thank Phil Scott and Tristan Crolard for their cooperation over the years on the topics of this paper. We had useful conversations with Federico Aschieri, Corrado Biasi, Alessandra Carbone, Carlo Dalla Pozza, Giuditta Franco, Hugo Herbelin, Neil Jones, Damiano Macedonio, Vincenzo Manca, Massimo Merro, Michel Parigot, Andy Pitts, Kurt Ranalter, Carolyn Talcott and Graham White. We thank an anonymous referee for helpful suggestions.
Abstract: We reconsider work by Bellin and Scott in the 1990s on R. Milner and S. Abramsky's encoding of linear logic in the π-calculus and give an account of efforts to establish a tight connection between the structure of proofs and of the cut elimination process in multiplicative linear logic, on one hand, and the input-output behaviour of the processes that represent them, on the other, resulting in a proof-theoretic account of (a variant of) Chu's construction. But Milner's encoding of the linear lambda calculus suggests consideration of multiplicative co-intuitionistic linear logic: we provide a term assignment for it, a calculus of coroutines which presents features of concurrent and distributed computing. Finally, as a test case of its adequacy as a logic for distributed computation, we represent our term assignment as a λP system. We argue that translations of typed functional languages in concurrent and distributed systems (such as π-calculi or λP systems) are best typed with co-intuitionistic logic, where some features of computations match the logical properties in a natural way.
