CMU-CS-03-131
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-03-131

A Judgmental Analysis of Linear Logic

Bor-Yuh Evan Chang, Kaustuv Chaudhuri, Frank Pfenning

April 2003

CMU-CS-03-131.ps
CMU-CS-03-131.pdf


Keywords: Constructive logic, linear logic, judgmental foundations


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