Skip to main content
SpringerLink
Log in

A mixed linear and non-linear logic: Proofs, terms and models

Extended abstract

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1994)

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

Included in the following conference series:

Abstract

Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad.

This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.

A considerably longer version of this paper is available as a University of Cambridge technical report

Research supported by a SERC Fellowship and the EU Esprit project LOMAPS.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Barendsen and S. Smetsers. Conventional and uniqueness typing in graph rewrite systems. Technical Report CSI-R9328, Katholieke Universiteit Nijmegen, December 1993.

    Google Scholar 

  2. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models (preliminary report). Technical Report 352, Computer Laboratory, University of Cambridge, September 1994.

    Google Scholar 

  3. P. N. Benton. Strong normalisation for the linear term calculus. Journal of Functional Programming, 1995. To appear. Also available as Technical Report 305, University of Cambridge Computer Laboratory, July 1993.

    Google Scholar 

  4. P. N. Benton, G. M. Bierman, J. M. E. Hyland, and V. C. V. de Paiva. Linear lambda calculus and categorical models revisited. In E. Börger et al., editor, Selected Papers from Computer Science Logic '92, volume 702 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

    Google Scholar 

  5. P. N. Benton, G. M. Bierman, J. M. E. Hyland, and V. C. V. de Paiva. A term calculus for intuitionistic linear logic. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

    Google Scholar 

  6. G. M. Bierman. On intuitionistic linear logic (revised version of PhD thesis). Technical Report 346, Computer Laboratory, University of Cambridge, August 1994.

    Google Scholar 

  7. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

    Article  Google Scholar 

  8. J.-Y. Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.

    Article  Google Scholar 

  9. B. Jacobs. Conventional and linear types in a logic of coalgebras. Preprint, University of Utrecht, April 1993.

    Google Scholar 

  10. P. Lincoln and J. C. Mitchell. Operational aspects of linear lambda calculus. In Proceedings of the 7th Annual Symposium on Logic in Computer Science. IEEE, 1992.

    Google Scholar 

  11. E. Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

    Article  Google Scholar 

  12. G. D. Plotkin. Type theory and recursion (abstract). In Proceedings of 8th Conference on Logic in Computer Science. IEEE Computer Society Press, 1993.

    Google Scholar 

  13. R. A. G. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Conference on Categories in Computer Science and Logic, volume 92 of AMS Contemporary Mathematics, June 1980.

    Google Scholar 

  14. P. Wadler. There's no substitute for linear logic (projector slides). In G. Winskel, editor, Proceedings of the CLICS Workshop (Part I), March 1992, Aarhus, Denmark, May 1992. Available as DAIMI PB-397-I Computer Science Department, Aarhus University.

    Google Scholar 

  15. P. Wadler. A taste of linear logic. In A. M. Borzyszkowski and S. Sokolowski, editors, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, number 711 in Lecture Notes in Computer Science, pages 185–210, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge, New Museums Site, Pembroke Street, CB2 3QG, Cambridge, UK

    P. N. Benton

Authors
  1. P. N. Benton
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Leszek Pacholski Jerzy Tiuryn

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Benton, P.N. (1995). A mixed linear and non-linear logic: Proofs, terms and models. In: Pacholski, L., Tiuryn, J. (eds) Computer Science Logic. CSL 1994. Lecture Notes in Computer Science, vol 933. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022251

Download citation

  • DOI: https://doi.org/10.1007/BFb0022251

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60017-6

  • Online ISBN: 978-3-540-49404-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation