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)
Abstract
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
Pointers to Related Work
- A. Barber and
G. Plotkin,
Dual Intuitionistic Linear Logic.
Submitted for publication, 1997.
- M. Hasegawa,
Categorical glueing and logical
predicates for models of linear logic.
Preprint RIMS-1223, Kyoto University, 1999.
- M. Hasegawa,
Girard translation and logical
predicates.
Journal
of Functional Programming 10(1): 77-89, 2000.
- T. Streicher,
Denotational completeness revisited.
In Proc. CTCS'99,
Electronic Notes in Theoretical Computer Science
29, 1999.
- Audrey Tan,
Full Completeness Results for Models of Linear Logic.
PhD thesis, Cambridge, 1997.
Back to Hassei's
Research Page / Home Page