{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:59Z","timestamp":1759638839123},"reference-count":19,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":6120,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1992,6]]},"abstract":"<jats:p>A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. Using the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC's. Using the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having \u201cinvertible\u201d proofs between the two terms. Work of Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.<\/jats:p>","DOI":"10.1017\/s0960129500001444","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:02:25Z","timestamp":1236157345000},"page":"231-247","source":"Crossref","is-referenced-by-count":34,"title":["Provable isomorphisms of types"],"prefix":"10.1017","volume":"2","author":[{"given":"Kim B.","family":"Bruce","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Di Cosmo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Longo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500001444_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BF02023009"},{"key":"S0960129500001444_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BF01084396"},{"key":"S0960129500001444_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_117"},{"key":"S0960129500001444_ref016","article-title":"Using types as search keys in function libraries","volume":"1","author":"Rittri","year":"1989","journal-title":"Journal of Functional Programming"},{"key":"S0960129500001444_ref015","doi-asserted-by":"crossref","unstructured":"Reynolds J.C. (1984) Polymorphism is not set-theoretic. Lecture Notes in Computer Science, 173.","DOI":"10.1007\/3-540-13346-1_7"},{"key":"S0960129500001444_ref012","volume-title":"Strong equivalence in positive propositional logic: provable realizability and type assignment","author":"Martini","year":"1991"},{"key":"S0960129500001444_ref011","first-page":"778","article-title":"Axiomatic bases for equational theories of natural numbers","volume":"19","author":"Martin","year":"1972","journal-title":"Notices of the Am. Math. Soc."},{"key":"S0960129500001444_ref010","volume-title":"An introduction to higher order categorical logic","author":"Lambek","year":"1986"},{"key":"S0960129500001444_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0075313"},{"key":"S0960129500001444_ref006","first-page":"291","volume-title":"ICALP","author":"Curien","year":"1991"},{"key":"S0960129500001444_ref003","volume-title":"The Lambda Calculus; Its syntax and Semantics (revised edition)","author":"Barendregt","year":"1984"},{"key":"S0960129500001444_ref013","unstructured":"Narendran P. , Pfenning F. and Statman R. (1989) On the unification problem for cartesian closed categories. Hardware Verification Workshop, 09 1989."},{"key":"S0960129500001444_ref008","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90085-2"},{"key":"S0960129500001444_ref004","doi-asserted-by":"crossref","unstructured":"Bruce K. and Longo G. (1985) Provable isomorphisms and domain equations in models of typed languages. ACM Symposium on Theory of Computing (STOC 85).","DOI":"10.1145\/22145.22175"},{"key":"S0960129500001444_ref002","volume-title":"Categories, Types, and Structures","author":"Asperti","year":"1991"},{"key":"S0960129500001444_ref014","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883461"},{"key":"S0960129500001444_ref007","unstructured":"Di Cosmo R. and Longo G. (1989) Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). Workshop on Logic for Computer Science \u2013 MSRI, Berkeley."},{"key":"S0960129500001444_ref005","unstructured":"Babaev A. A. and Soloviev S. V. (1982) Coherence theorem for canonical maps in certesian closed categories. Journal of Soviet Mathematics, 20."},{"key":"S0960129500001444_ref001","doi-asserted-by":"crossref","unstructured":"Alessi F. and Barbanera F. (1991) Strong conjunction and intersection types. Dipartimento di Informatica, Universit\u00e0 di Torino (Italy), manuscript.","DOI":"10.1007\/3-540-54345-7_49"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500001444","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T07:04:12Z","timestamp":1684911852000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500001444\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,6]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1992,6]]}},"alternative-id":["S0960129500001444"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500001444","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,6]]}}}