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 [4].
Publication Year: 1996
Publication Date: 1996-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 174
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot