Publications

Authors:

Bellin, Gianluigi; Menti, Alessandro

Title:

On the π-calculus and Co-intuitionistic Logic. Notes on Logic for Concurrency and λP Systems

Year:

2014

Type of item:

Articolo in Rivista

Tipologia ANVUR:

Articolo su rivista

Language:

Inglese

Format:

A Stampa

Referee:

Sì

Name of journal:

Fundamenta Informaticae

ISSN of journal:

0169-2968

N° Volume:

130

Number or Folder:

1

:

IOS Press

Page numbers:

21-65

Keyword:

Logica; Informatica

Short description of contents:

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.

Web page:

http://dx.doi.org/10.3233/FI-2014-981

Product ID:

85713

Handle IRIS:

11562/883991

Deposited On:

February 4, 2015

Last Modified:

November 15, 2022

Bibliographic citation:

Bellin, Gianluigi; Menti, Alessandro, On the π-calculus and Co-intuitionistic Logic. Notes on Logic for Concurrency and λP Systems «Fundamenta Informaticae» , vol. 130 , n. 1 , 2014 , pp. 21-65

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo