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 linear ones. So while the semantics of DILL can be given in terms of monoidal adjunctions between symmetric monoidal closed categories and cartesian closed categories, the semantics of ILT is better presented via fibrations. These interpret double contexts, which cannot be reduced to linear ones. In order to interpret the intuitionistic and linear identity axioms acting on the same type we need fibrations satisfying the comprehension axiom. Research supported by EPSRC-grant GR/L28296 under the title “The eXplicit Substitution Linear Abstract Machine”.

Categorical models for intuitionistic and linear type theory

MAIETTI, MARIA EMILIA;
2000

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 linear ones. So while the semantics of DILL can be given in terms of monoidal adjunctions between symmetric monoidal closed categories and cartesian closed categories, the semantics of ILT is better presented via fibrations. These interpret double contexts, which cannot be reduced to linear ones. In order to interpret the intuitionistic and linear identity axioms acting on the same type we need fibrations satisfying the comprehension axiom. Research supported by EPSRC-grant GR/L28296 under the title “The eXplicit Substitution Linear Abstract Machine”.
2000
Foundations of Software Science and Computation Structures
9783540672579
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/1357342
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact