*Abstract:*

We present a new intuitionistic linear logic, Dual
Intuitionistic Linear Logic, designed to reflect the motivation of
exponentials as translations of intuitionistic types, and provide
it with a term calculus, proving associated standard type-theoretic
results. We give a sound and complete categorical semantics for the
type-system, and consider the relationship of the new type-theory
to the more familiar presentation found for example in ``A term
calculus for intuitionistic linear logic'' by Benton *et
al*.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file