Logical predicates for intuitionistic linear type theories

Masahito Hasegawa

In Proc. 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), Springer LNCS 1581, pages 198-213 (1999)


We develop a notion of Kripke-like parameterized logical predicates for two fragments of intuitionistic linear logic (MILL and DILL) in terms of their category-theoretic models. Such logical predicates are derived from the categorical glueing construction combined with the free symmetric monoidal cocompletion. As applications, we obtain full completeness results of translations between linear type theories.

© Springer-Verlag 1999

[gzipped ps file] [pdf file]

Pointers to Related Work

Back to Hassei's Research Page / Home Page