A language for multiplicative-additive linear logic

  • Cockett J
  • Pastro C
  • 5


    Mendeley users who have this article in their library.
  • 5


    Citations of this article.


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. © 2005 Elsevier B.V. All rights reserved.

Author-supplied keywords

  • Linearly distributive categories
  • Multiplicative-additive linear logic
  • Process semantics
  • Rewriting modulo equations
  • Term logic

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • J. R.B. Cockett

  • C. A. Pastro

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free