A language for multiplicative-additive linear logic

J. R.B. Cockett, C. A. Pastro

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

5 引用 (Scopus)

抄録

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 20048 14 2004

Fingerprint

Linear Logic
Multiplicative
Calculus
Rewriting Systems
Cut-elimination
Term
Concurrency
Computer programming languages
Programming Languages
Modulo
Linearly
Semantics
Equivalence
Language

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

これを引用

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

:: Electronic Notes in Theoretical Computer Science, 巻 122, 07.03.2005, p. 23-65.

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

Cockett, J. R.B. ; Pastro, C. A. / A language for multiplicative-additive linear logic. :: Electronic Notes in Theoretical Computer Science. 2005 ; 巻 122. pp. 23-65.
@article{1b3c3c4afadf4fa88dcaae8635c2709a,
title = "A language for multiplicative-additive linear logic",
abstract = "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.",
author = "Cockett, {J. R.B.} and Pastro, {C. A.}",
year = "2005",
month = "3",
day = "7",
doi = "10.1016/j.entcs.2004.06.049",
language = "English",
volume = "122",
pages = "23--65",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

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 -