{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T21:31:41Z","timestamp":1762032701266},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_18","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T11:30:26Z","timestamp":1196508626000},"page":"250-265","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Linear Logical View of Linear Type Isomorphisms"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Balat","sequence":"first","affiliation":[]},{"given":"Roberto","family":"Di Cosmo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"18_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0026989","volume-title":"Category Theory and Computer Science","author":"A. Andreev","year":"1997","unstructured":"A. Andreev and S. Soloviev. A deciding algorithm for linear isomorphism of types with complexity o(nlog\n2(n)). In E. Moggi and G. Rossolini, editors, Category Theory and Computer Science, number 1290 in LNCS, pages 197\u2013210"},{"key":"18_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-61756-6_95","volume-title":"Programming Languages Implementation and Logic Programming (PLILP)","author":"M.-V. Aponte","year":"1996","unstructured":"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\u2013346. Springer-Verlag, 1996."},{"key":"18_CR3","unstructured":"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\u201387. Cambridge University Press, 1985."},{"issue":"2","key":"18_CR4","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1017\/S0960129500001444","volume":"2","author":"K. Bruce","year":"1992","unstructured":"K. Bruce, R. Di Cosmo, and G. Longo. Provable isomorphisms oft ypes. Mathematical Structures in Computer Science, 2(2):231\u2013247, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/22145.22175"},{"key":"18_CR6","unstructured":"D. Delahaye, R. Di Cosmo, and B. Werner. Recherche dans une biblioth\u00e8que de preuves Coq en utilisant le type et modulo isomorphismes. In PRC\/GDR de programmation, P\u00f4le Preuves et Sp\u00e9cifications Alg\u00e9briques, November 1997."},{"key":"18_CR7","unstructured":"R. Di Cosmo. Invertibility ofterms and valid isomorphisms. a prooftheoretic study on second order \u03bb-calculus with surjective pairing and terminal object. Technical Report 91-10, LIENS-Ecole Normale Sup\u00e9rieure, 1991."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo. Type isomorphisms in a type assignment framework. In 19th Ann. ACM Symp. on Principles of Programming Languages (POPL), pages 200\u2013210. ACM, 1992.","DOI":"10.1145\/143165.143208"},{"issue":"3","key":"18_CR9","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1017\/S0956796800000861","volume":"3","author":"R. Cosmo Di","year":"1993","unstructured":"R. Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485\u2013525, 1993. Special Issue on ML.","journal-title":"Journal of Functional Programming"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo. Isomorphisms of types: from \u03bb-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.","DOI":"10.1007\/978-1-4612-2572-0"},{"key":"18_CR11","series-title":"Mathematical Sciences Research Institute Publications","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-1-4612-2822-6_4","volume-title":"Logic from Computer Science","author":"R. Cosmo Di","year":"1991","unstructured":"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\u201394. Springer Verlag, Berkeley, 1991."},{"key":"18_CR12","unstructured":"K. Dosen and Z. Petric. Isomorphic objects in symmetric monoidal closed categories. Technical Report 95-49-R, IRIT, 1995."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.","DOI":"10.1016\/0304-3975(87)90045-4"},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0022-4049(71)90013-2","volume":"1","author":"S. M. Lane","year":"1971","unstructured":"S. Mac Lane and G. M. Kelly. Coherence in Closed Categories. Journal of Pure and Applied Algebra, 1(1):97\u2013140, 1971.","journal-title":"Journal of Pure and Applied Algebra"},{"issue":"7","key":"18_CR15","first-page":"778","volume":"19","author":"C. F. Martin","year":"1972","unstructured":"C. F. Martin. Axiomatic bases for equational theories of natural numbers. Notices of the Am. Math. Soc., 19(7):778, 1972.","journal-title":"Notices of the Am. Math. Soc"},{"key":"18_CR16","volume-title":"Universal type isomorphisms in cartesian closed categories","author":"L. Meertens","year":"1990","unstructured":"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."},{"key":"18_CR17","series-title":"Lect Notes Comput Sci","volume-title":"10th Int. Conf. on Automated Deduction","author":"M. Rittri","year":"1990","unstructured":"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."},{"key":"18_CR18","series-title":"PhD thesis","volume-title":"Searching program libraries by type and proving compiler correctness by bisimulation","author":"M. Rittri","year":"1990","unstructured":"M. Rittri. Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University ofG\u00f6teborg, G\u00f6teborg, Sweden, 1990."},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S095679680000006X","volume":"1","author":"M. Rittri","year":"1991","unstructured":"M. Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71\u201389, 1991.","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"18_CR20","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S0956796800020049","volume":"1","author":"2. C. Runciman","year":"1991","unstructured":"[20] C. Runciman and I. Toyn. Retrieving re-usable software components by polymorphic type. Journal of Functional Programming, 1(2):191\u2013211, 1991.","journal-title":"Journal of Functional Programming"},{"issue":"3","key":"18_CR21","doi-asserted-by":"publisher","first-page":"1387","DOI":"10.1007\/BF01084396","volume":"22","author":"S. V. Soloviev","year":"1983","unstructured":"S. V. Soloviev. The category offinite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387\u20131400, 1983.","journal-title":"Journal of Soviet Mathematics"},{"key":"18_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/3-540-56944-8_71","volume-title":"Logic Programming and Automated Reasoning, 4th International Conference","author":"S. V. Soloviev","year":"1993","unstructured":"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\u2013371, St. Petersburg, Russia, 1993. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T04:08:49Z","timestamp":1586146129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}