Categorical Models for Intuitionistic and Linear Type Theory

@article{citeulike:401375, abstract = {This paper describes the categorical semantics of a system of mixed intuitionistic and linear type theory (ILT). ILT was proposed by G. Plotkin and also independently by P. Wadler. The logic associated with ILT is obtained as a combination of intuitionistic logic with intuitionistic linear logic, and can be embedded in Barber and Plotkin's Dual Intuitionistic Linear Logic (DILL). However, unlike DILL, the logic for ILT lacks an explicit modality ! that translates intuitionistic proofs into...}, author = {Maietti, Maria E. and de Paiva, Valeria and Ritter, Eike }, citeulike-article-id = {401375}, journal = {Lecture Notes in Computer Science}, keywords = {categorical, linear, logic}, posted-at = {2005-11-19 17:01:55}, priority = {0}, title = {Categorical Models for Intuitionistic and Linear Type Theory}, url = {http://citeseer.ist.psu.edu/maietti00categorical.html}, volume = {1784}, year = {2000} }

TY - JOUR ID - citeulike:401375 L3 - citeulike-article-id:401375 N2 - This paper describes the categorical semantics of a system of mixed intuitionistic and linear type theory (ILT). ILT was proposed by G. Plotkin and also independently by P. Wadler. The logic associated with ILT is obtained as a combination of intuitionistic logic with intuitionistic linear logic, and can be embedded in Barber and Plotkin's Dual Intuitionistic Linear Logic (DILL). However, unlike DILL, the logic for ILT lacks an explicit modality ! that translates intuitionistic proofs into... JF - Lecture Notes in Computer Science TI - Categorical Models for Intuitionistic and Linear Type Theory VL - 1784 KW - categorical KW - linear KW - logic AU - Maietti, Maria AU - de Paiva, Valeria AU - Ritter, Eike PY - 2000/// UR - http://citeseer.ist.psu.edu/maietti00categorical.html ER -