Skip to main content
SpringerLink
Log in

A Linear Logical View of Linear Type Isomorphisms

  • Conference paper
  • First Online:
Book cover Computer Science Logic (CSL 1999)

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

Included in the following conference series:

Abstract

The notion of isomorphisms of types has many theoretical as well as practical consequences, and isomorphisms of types have been investigated at length over the past years. Isomorphisms in weak system (like linear lambda calculus) have recently been investigated due to their practical interest in library search. In this paper we give a remarkably simple and elegant characterization of linear isomorphisms in the setting of Multiplicative Linear Logic (MLL), by making an essential use ofthe correctness criterion for Proof Nets due to Girard.

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. A. Andreev and S. Soloviev. A deciding algorithm for linear isomorphism of types with complexity o(nlog 2(n)). In E. Moggi and G. Rossolini, editors, Category Theory and Computer Science, number 1290 in LNCS, pages 197–210

    Chapter  Google Scholar 

  2. M.-V. Aponte and R. Di Cosmo. Type isomorphisms for module signatures. In Programming Languages Implementation and Logic Programming (PLILP), volume 1140 of Lecture Notes in Computer Science, pages 334–346. Springer-Verlag, 1996.

    Chapter  Google Scholar 

  3. G. Berry and P.-L. Curien. Theory and practice ofsequen tial algorithms: the kernel ofthe applicative language CDS. In M. Nivat and J. Reynolds, editors, Algebraic methods in semantics, pages 35–87. Cambridge University Press, 1985.

    Google Scholar 

  4. K. Bruce, R. Di Cosmo, and G. Longo. Provable isomorphisms oft ypes. Mathematical Structures in Computer Science, 2(2):231–247, 1992.

    Article  MathSciNet  Google Scholar 

  5. K. Bruce and G. Longo. Provable isomorphisms and domain equations in models oft yped languages. ACM Symposium on Theory of Computing (STOC 85), May 1985.

    Google Scholar 

  6. D. Delahaye, R. Di Cosmo, and B. Werner. Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes. In PRC/GDR de programmation, Pôle Preuves et Spécifications Algébriques, November 1997.

    Google Scholar 

  7. R. Di Cosmo. Invertibility ofterms and valid isomorphisms. a prooftheoretic study on second order λ-calculus with surjective pairing and terminal object. Technical Report 91-10, LIENS-Ecole Normale Supérieure, 1991.

    Google Scholar 

  8. R. Di Cosmo. Type isomorphisms in a type assignment framework. In 19th Ann. ACM Symp. on Principles of Programming Languages (POPL), pages 200–210. ACM, 1992.

    Google Scholar 

  9. R. Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485–525, 1993. Special Issue on ML.

    Article  MathSciNet  Google Scholar 

  10. R. Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.

    Google Scholar 

  11. R. Di Cosmo and G. Longo. Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). In Moschovakis, editor, Logic from Computer Science, volume 21 of Mathematical Sciences Research Institute Publications, pages 73–94. Springer Verlag, Berkeley, 1991.

    Chapter  Google Scholar 

  12. K. Dosen and Z. Petric. Isomorphic objects in symmetric monoidal closed categories. Technical Report 95-49-R, IRIT, 1995.

    Google Scholar 

  13. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.

    Google Scholar 

  14. S. Mac Lane and G. M. Kelly. Coherence in Closed Categories. Journal of Pure and Applied Algebra, 1(1):97–140, 1971.

    Article  MathSciNet  Google Scholar 

  15. C. F. Martin. Axiomatic bases for equational theories of natural numbers. Notices of the Am. Math. Soc., 19(7):778, 1972.

    Google Scholar 

  16. L. Meertens and A. Siebes. Universal type isomorphisms in cartesian closed categories. Centrum voor Wiskunde en Informatica, Amsterdam, the Netherlands. E-mail: lambert,arno@cwi.nl, 1990.

    Google Scholar 

  17. M. Rittri. Retrieving library identifiers by equational matching oft ypes in 10th Int. Conf. on Automated Deduction. Lecture Notes in Computer Science, 449, July 1990.

    Google Scholar 

  18. M. Rittri. Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University ofGöteborg, Göteborg, Sweden, 1990.

    Google Scholar 

  19. M. Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71–89, 1991.

    Article  MathSciNet  Google Scholar 

  20. [20] C. Runciman and I. Toyn. Retrieving re-usable software components by polymorphic type. Journal of Functional Programming, 1(2):191–211, 1991.

    Article  MathSciNet  Google Scholar 

  21. S. V. Soloviev. The category offinite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387–1400, 1983.

    Article  Google Scholar 

  22. S. V. Soloviev. A complete axiom system for isomorphism of types in closed categories. In A. Voronkov, editor, Logic Programming and Automated Reasoning, 4th International Conference, volume 698 of Lecture Notes in Artificial Intelligence (subseries of LNCS), pages 360–371, St. Petersburg, Russia, 1993. Springer-Verlag.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIENS École normale supérieure, 45 rue d’Ulm, 75005, Paris, France

    Vincent Balat & Roberto Di Cosmo

Authors
  1. Vincent Balat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roberto Di Cosmo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematisches Institut, Universität Freiburg, Eckerstr. 1, D-79104, Freiburg, Germany

    Jörg Flum

  2. Dpto. de Sistemas Informáticos y Programación Edificio Fac. Matemáticas, Universidad Complutense de Madrid, Av. Complutense s/n, E-28040, Madrid, Spain

    Mario Rodriguez-Artalejo

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Balat, V., Di Cosmo, R. (1999). A Linear Logical View of Linear Type Isomorphisms. In: Flum, J., Rodriguez-Artalejo, M. (eds) Computer Science Logic. CSL 1999. Lecture Notes in Computer Science, vol 1683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48168-0_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-48168-0_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48168-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation