Skip to main content
SpringerLink
Log in

Rewriting properties of combinators for rudimentary linear logic

  • Conference paper
  • First Online:
Higher-Order Algebra, Logic, and Term Rewriting (HOA 1993)

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

  • 139 Accesses

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. M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, ‘Explicit substitutions', in Journal of Functional Programming, 1991, Vol. 1, No. 4, pp. 375–416.

    Google Scholar 

  2. N. Benton, G. Bierman, V. de Paiva, M. Hyland, ‘Term assignment for intuitionistic linear logic', Technical Report No. 262, Computer Laboratory, University of Cambridge, 1992.

    Google Scholar 

  3. G. Bierman, ‘On Intuitionistic Linear Logic', Draft of Ph.D. Thesis, Computer Laboratory, University of Cambridge, 1993.

    Google Scholar 

  4. T. Coquand, Th. Ehrhard, ‘An equational presentation of higher order logic', in Proceedings of Category Theory and Computer Science, Lecture Notes in Computer Science 283, Springer-Verlag, 1987, pp. 40–56.

    Google Scholar 

  5. G. Cousineau, P.-L. Curien, M. Mauny, ‘The categorical abstract machine', in Science of Computer Programming, 1987, Vol. 8, pp. 173–202.

    Google Scholar 

  6. P.-L. Curien, ‘Categorical Combinators, Sequential Algorithms and Functional Programming', Birkhäuser, 1993.

    Google Scholar 

  7. P.-L. Curien, T. Hardin, A. Ríos, 'strong normalisation of substitutions', in Proceedings of the 17th International Symposium on Mathematical Foundations of Computer Science 1992, Lecture Notes in Computer Science 629, Springer-Verlag, 1992, pp. 209–217.

    Google Scholar 

  8. N. Dershowitz, J.-P. Jouannaud, ‘Rewrite Systems', in Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, J. van Leeuwen (ed.), North-Holland, 1990, pp. 243–320.

    Google Scholar 

  9. Th. Ehrhard, ‘A categorical semantics of constructions', in Proceedings of the 3rd Annual Symposium on Logic in Computer Science, IEEE, 1988, pp. 264–273.

    Google Scholar 

  10. S. J. Garland, J. V. Guttag, ‘A Guide to LP, The Larch Prover', Release 2.2 LP Documentation, MIT, November 1991.

    Google Scholar 

  11. J.-Y. Girard, ‘Linear logic', in Theoretical Computer Science, 1987, Vol. 50, pp. 1–102.

    Google Scholar 

  12. J.-Y. Girard, P. Taylor, Y. Lafont, ‘Proofs and Types', Cambridge University Press, 1989.

    Google Scholar 

  13. T. Hardin, ‘Confluence results for the pure strong categorical logic CCL. λ-calculi as subsystems of CCL', in Theoretical Computer Science, 1989, Vol. 65, pp. 291–342.

    Google Scholar 

  14. T. Hardin, A. Laville, ‘Proof of termination of the rewriting system Subst on CCL', in Theoretical Computer Science, 1986, Vol. 46, pp. 305–312.

    Google Scholar 

  15. M. Hermann, ‘Vademecum of Divergent Term Rewriting Systems', Technical Report CRIN 88-R-082, Centre de Recherche en Informatique de Nancy, 1988.

    Google Scholar 

  16. M. Hermann, ‘Chain Properties of Rule Closures', in Formal Aspects of Computing, 1990, Vol. 2, pp. 207–225.

    Google Scholar 

  17. Y. Lafont, ‘The linear abstract machine', in Theoretical Computer Science, 1988, Vol. 59, pp. 157–180.

    Google Scholar 

  18. V. de Paiva, E. Ritter, ‘Categorical combinators for symmetric multicategories', unpublished manuscript, 1994.

    Google Scholar 

  19. E. Ritter, ‘Categorical Abstract Machines for Higher-Order Lambda Calculi', to appear in Theoretical Computer Science. Also available as Technical Report No. 297, Computer Laboratory, University of Cambridge, 1993.

    Google Scholar 

  20. E. Ritter, ‘Normalization for Typed Lambda Calculi with Explicit Substitution', to appear in Proceedings of the 1993 Annual Conference of the European Association for Computer Science Logic CSL 93, Lecture Notes in Computer Science.

    Google Scholar 

  21. E. Ritter, V. de Paiva, 'syntactic Multicategories and Categorical Combinators for Linear Logic', presented at the Fifth Biennial Meeting on Category Theory and Computer Science CTCS-5, Amsterdam, September 1993.

    Google Scholar 

  22. A. Scedrov, ‘A Brief Guide to Linear Logic', in Bulletin of EATCS, No. 41, June 1990, pp. 154–165.

    Google Scholar 

  23. H. Zantema, ‘Termination of term rewriting by interpretation', in Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems CTRS-92, Lecture Notes in Computer Science 656, Springer-Verlag, 1993, pp. 155–167.

    Google Scholar 

  24. H. Zantema, Private Communication, June 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge, UK

    Monica Nesi & Valeria de Paiva

  2. Computing Laboratory, Oxford University, UK

    Eike Ritter

Authors
  1. Monica Nesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Valeria de Paiva
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eike Ritter
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan Heering Karl Meinke Bernhard Möller Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nesi, M., de Paiva, V., Ritter, E. (1994). Rewriting properties of combinators for rudimentary linear logic. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds) Higher-Order Algebra, Logic, and Term Rewriting. HOA 1993. Lecture Notes in Computer Science, vol 816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58233-9_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-58233-9_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58233-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation