Dual Intuitionistic Linear Logic

Andrew Barber


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:

Previous | Index | Next