We reexamine the foundations of linear logic, developing a system of natural deduction following Martin-Lof s separation of judgments from propositions. Our construction yields a clean and elegant formulation that accounts for a rich set of multiplicative, additive, and exponential connectives, extending dual intuitionistic linear logic but differing from both classical linear logic and Hyland and de Paiva s full intuitionistic linear logic. We also provide a corresponding sequent calculus that admits a simple proof of the admissibility of cut by a single structural induction. Finally, we show how to interpret classical linear logic (with or without the MIX rule) in our system, employing a form of double-negation translation.

25 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu