TY - JOUR
T1 - A language for multiplicative-additive linear logic
AU - Cockett, J. R.B.
AU - Pastro, C. A.
N1 - Funding Information:
1 Research partially supported by NSERC, Canada. Diagrams were produced with the XY-pic package of K. Rose and R. Moore and inferences with M. Tatsuya’s proof.sty. 2 Email: robin@cpsc.ucalgary.ca 3 Email: pastroc@cpsc.ucalgary.ca
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
SN - 1571-0661
VL - 122
SP - 23
EP - 65
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
T2 - Proceedings of the 10th Conference on Category Theory in Computer Science (CTCS 2004)
Y2 - 12 August 2004 through 14 August 2004
ER -