Skip to main content
SpringerLink
Log in

Logical Predicates for Intuitionistic Linear Type Theories

  • Conference paper
  • First Online:
Book cover Typed Lambda Calculi and Applications (TLCA 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1581))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S., Gay, S.J., and Nagarajan, R. (1996), Specification structures and propositions-as-types for concurrency, in “Proceedings, 8th Banff Higher Order Workshop”, Springer LNCS 1043, pp. 5–40.

    Google Scholar 

  2. Alimohamed, M. (1995), A characterization of lambda definability in categorical models of implicit polymorphism, Theoret. Comp. Sci. 146, 5–23.

    Article  MATH  MathSciNet  Google Scholar 

  3. Ambler, S.J. (1992), “First Order Linear Logic in Symmetric Monoidal Closed Categories”, Ph.D. thesis, ECS-LFCS-92-194, University of Edinburgh.

    Google Scholar 

  4. Barber, A., Gardner, P., Hasegawa, M., and Plotkin, G. (1998), From action calculi to linear logic, in “Computer Science Logic (CSL’97), Selected Papers”, Springer LNCS 1414, pp. 78–97.

    Google Scholar 

  5. Barber, A., and Plotkin, G. (1997), Dual intuitionistic linear logic, submitted.

    Google Scholar 

  6. Benton, N. (1995), A mixed linear non-linear logic: proofs, terms and models, in “Computer Science Logic (CSL’94), Selected Papers”, Springer LNCS 933, pp. 121–135.

    Google Scholar 

  7. Benton, N., Bierman, G.M., de Paiva, V., and Hyland, J.M.E. (1993), Linear lambda-calculus and categorical models revisited, in “Computer Science Logic (CSL’92), Selected Papers”, Springer LNCS 702, pp. 61–84.

    Google Scholar 

  8. Bierman, G.M. (1995), What is a categorical model of intuitionistic linear logic? in “Proceedings, Typed Lambda Calculi and Applications (TLCA’95)”, Springer LNCS 902, pp. 78–93.

    Chapter  Google Scholar 

  9. Blute, R.F., Scott, P.J. (1996), Linear Läuchli semantics, Ann. Pure Appl. Logic 77, 229–296.

    Article  MathSciNet  Google Scholar 

  10. Eilenberg, S., and Kelly, G.M. (1966), Closed categories, in “Proceedings, Categorical Algebra (La Jolla 1965)”, pp. 421–562, Springer-Verlag.

    Google Scholar 

  11. Garrigue, J., and Minamide, Y. (1998), On the runtime complexity of type-directed unboxing, in “Proceedings, International Conference on Functional Programming (ICFP’98)”, pp. 1–12, ACM Press.

    Google Scholar 

  12. Girard, J.-Y. (1987), Linear logic, Theoret. Comp. Sci. 50, 1–102.

    Article  MATH  MathSciNet  Google Scholar 

  13. Hasegawa, M. (1999), Categorical glueing and logical predicates for models of linear logic, technical report, RIMS, Kyoto University.

    Google Scholar 

  14. Hermida, C. (1994), “Fibrations, Logical Predicates and Indeterminates”, Ph.D. thesis, ECS-LFCS-93-277, University of Edinburgh.

    Google Scholar 

  15. Im, G.B., and Kelly, G.M. (1986), A universal property of the convolution monoidal structure, J. Pure Appl. Algebra 43, 75–88.

    Article  MATH  MathSciNet  Google Scholar 

  16. Lafont, Y. (1988), “Logiques, Catégories et Machines”, Thèse de Doctorat, Université Paris VII.

    Google Scholar 

  17. Lambek, J. (1995), Bilinear logic in algebra and linguistics, in “Advances in Linear Logic”, pp. 43–59, Cambridge University Press.

    Google Scholar 

  18. Loader, R. (1994), “Models of Lambda Calculi and Linear Logic: Structural, Equational and Proof-Theoretic Characterisations”, Ph.D. thesis, Oxford University.

    Google Scholar 

  19. Mac Lane, S. (1971), “Categories for theWorking Mathematician”, Graduate Texts in Mathematics 5, Springer-Verlag.

    Google Scholar 

  20. Milner, R. (1996), Calculi for interaction, Acta Inform. 33(8), 707–737.

    Article  MathSciNet  Google Scholar 

  21. Mitchell, J.C., and Scedrov, A. (1992), Notes on sconing and relators, in “Computer Science Logic (CSL’92), Selected Papers”, Springer LNCS 702, pp. 352–378.

    Google Scholar 

  22. Power, A.J. (1996), Elementary control structures, in “Proceedings, Concurrency Theory (CONCUR’96)”, Springer LNCS 1119, pp. 115–130.

    Google Scholar 

  23. Tan, A.M. (1997), “Full Completeness for Models of Linear Logic”, Ph.D. thesis, University of Cambridge.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. RIMS, Kyoto University, Kyoto, 606-8502, Japan

    Masahito Hasegawa

Authors
  1. Masahito Hasegawa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS - UPR9016, Institut de Mathématiques de Luminy, 163 Avenue de Luminy, case 907, F-13288, Marseille cedex 9, France

    Jean-Yves Girard

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hasegawa, M. (1999). Logical Predicates for Intuitionistic Linear Type Theories. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-48959-2_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65763-7

  • Online ISBN: 978-3-540-48959-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation