### 抄録

A term calculus for the proofs in multiplicative-additive linear logic is introduced and motivated as a programming language for channel based concurrency. The term calculus is proved complete for a semantics in linearly distributive categories with additives. It is also shown that proof equivalence is decidable by showing that the cut elimination rewrites supply a confluent rewriting system modulo equations.

元の言語 | 英語 |
---|---|

ページ（範囲） | 23-65 |

ページ数 | 43 |

ジャーナル | Electronic Notes in Theoretical Computer Science |

巻 | 122 |

DOI | |

出版物ステータス | 出版済み - 3 7 2005 |

イベント | Proceedings of the 10th Conference on Category Theory in Computer Science (CTCS 2004) - 継続期間: 8 12 2004 → 8 14 2004 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

### これを引用

*Electronic Notes in Theoretical Computer Science*,

*122*, 23-65. https://doi.org/10.1016/j.entcs.2004.06.049

**A language for multiplicative-additive linear logic.** / Cockett, J. R.B.; Pastro, C. A.

研究成果: ジャーナルへの寄稿 › Conference article

*Electronic Notes in Theoretical Computer Science*, 巻. 122, pp. 23-65. https://doi.org/10.1016/j.entcs.2004.06.049

}

TY - JOUR

T1 - A language for multiplicative-additive linear logic

AU - Cockett, J. R.B.

AU - Pastro, C. A.

PY - 2005/3/7

Y1 - 2005/3/7

N2 - A term calculus for the proofs in multiplicative-additive linear logic is introduced and motivated as a programming language for channel based concurrency. The term calculus is proved complete for a semantics in linearly distributive categories with additives. It is also shown that proof equivalence is decidable by showing that the cut elimination rewrites supply a confluent rewriting system modulo equations.

AB - A term calculus for the proofs in multiplicative-additive linear logic is introduced and motivated as a programming language for channel based concurrency. The term calculus is proved complete for a semantics in linearly distributive categories with additives. It is also shown that proof equivalence is decidable by showing that the cut elimination rewrites supply a confluent rewriting system modulo equations.

UR - http://www.scopus.com/inward/record.url?scp=14544267593&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=14544267593&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2004.06.049

DO - 10.1016/j.entcs.2004.06.049

M3 - Conference article

AN - SCOPUS:14544267593

VL - 122

SP - 23

EP - 65

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -