Pubblicazioni

Autori:

Bellin, Gianluigi; Menti, Alessandro

Titolo:

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

Anno:

2014

Tipologia prodotto:

Articolo in Rivista

Tipologia ANVUR:

Articolo su rivista

Lingua:

Inglese

Formato:

A Stampa

Referee:

Sì

Nome rivista:

Fundamenta Informaticae

ISSN Rivista:

0169-2968

N° Volume:

130

Numero o Fascicolo:

1

Editore:

IOS Press

Intervallo pagine:

21-65

Parole chiave:

Logica; Informatica

Breve descrizione dei contenuti:

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.

Pagina Web:

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

Id prodotto:

85713

Handle IRIS:

11562/883991

depositato il:

4 febbraio 2015

ultima modifica:

15 novembre 2022

Citazione bibliografica:

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