We detail Abramsky's "proofs-as-processes" paradigm for interpreting linear logic (CLL) into a "synchronous" version of the pi-calculus proposed by Milner. The translation is given at the abstract level of proof structures. We give a detailed treatment of information flow in proof-nets and show how to mirror various evaluation strategies for proof normalization. Soundness and completeness results for the process-calculus translations of various fragments of CLL are given. The paper also gives a self-contained introduction to some of the deeper proof theory of CLL, and its process interpretation.
On the Pi-calculus and linear logic
BELLIN, Gianluigi;
1994-01-01
Abstract
We detail Abramsky's "proofs-as-processes" paradigm for interpreting linear logic (CLL) into a "synchronous" version of the pi-calculus proposed by Milner. The translation is given at the abstract level of proof structures. We give a detailed treatment of information flow in proof-nets and show how to mirror various evaluation strategies for proof normalization. Soundness and completeness results for the process-calculus translations of various fragments of CLL are given. The paper also gives a self-contained introduction to some of the deeper proof theory of CLL, and its process interpretation.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
1-s2.0-0304397594001049-main.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
4.85 MB
Formato
Adobe PDF
|
4.85 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
