{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:48:01Z","timestamp":1760078881287,"version":"3.28.0"},"reference-count":32,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2002.1029824","type":"proceedings-article","created":{"date-parts":[[2003,6,25]],"date-time":"2003-06-25T22:14:31Z","timestamp":1056579271000},"page":"147-156","source":"Crossref","is-referenced-by-count":4,"title":["Remarks on isomorphisms in typed lambda calculi with empty and sum types"],"prefix":"10.1109","author":[{"given":"M.","family":"Fiore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Di Cosmo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V.","family":"Balat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(90)90049-8"},{"journal-title":"Extensional normalisation for typed lambda calculus with sums via Grothendieck logical relations","year":"2002","author":"fiore","key":"17"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1985-0781071-1"},{"key":"15","doi-asserted-by":"crossref","first-page":"95","DOI":"10.4064\/fm-65-1-95-127","article-title":"An extended arithmetic of ordinal numbers","volume":"65","author":"doner","year":"1969","journal-title":"Fundamenta Mathematica"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002241"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2572-0","author":"di cosmo","year":"1995","journal-title":"Isomorphisms of types From ?-calculus to information retrieval and language design"},{"key":"14","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1006\/inco.1995.1085","article-title":"Second order isomorphic types. A proof theoretic study on second order ?-calculus with surjective pairing and terminal object","author":"di cosmo","year":"1995","journal-title":"Information and Computation"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000861"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000861"},{"key":"21","article-title":"Introduction to higher order categorical logic","volume":"7","author":"lambek","year":"1986","journal-title":"Cambridge Studies in Advanced Mathematics"},{"journal-title":"Logiques cate?gories et machines","year":"1987","author":"lafont","key":"20"},{"key":"22","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":"23","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287600"},{"key":"24","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-52885-7_117","article-title":"Retrieving library identifiers by equational matching of types","volume":"499","author":"rittri","year":"1990","journal-title":"Lecture Notes in Computer Science"},{"journal-title":"Searching program libraries by type and proving compiler correctness by bisimulation","year":"1990","author":"rittri","key":"25"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000006X"},{"key":"27","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1017\/S0956796800020049","article-title":"Retrieving re-usable software components by polymorphic type","volume":"1","author":"runciman","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(99)00185-1"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1007\/BF01084396"},{"key":"3","first-page":"57","article-title":"Type isomorphisms and proof reuse in dependent type theory","volume":"2030","author":"barthes","year":"2001","journal-title":"LNCS"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_18"},{"key":"10","article-title":"Recherche dans une bibliothe?que de preuves Coq en utilisant le type et modulo isomorphismes","author":"delahaye","year":"1997","journal-title":"PRC\/GDR de programmation Po?le Preuves et Spe?cifications Alge?briques"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61756-6_95"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56944-8_71"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(93)90035-R"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.2307\/2324454"},{"journal-title":"On exponentiation - A solution to Tarski's high school algebra problem","year":"1981","author":"wilkie","key":"32"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22175"},{"key":"31","article-title":"Practical foundations of mathematics","volume":"59","author":"taylor","year":"1999","journal-title":"Cambridge Studies in Advanced Mathematics"},{"key":"4","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1017\/S0960129500001444","article-title":"Provable isomorphisms of types","volume":"2","author":"bruce","year":"1992","journal-title":"Mathematical Structures in Computer Science"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172707"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000232"}],"event":{"name":"17th Annual IEEE Symposium on Logic in Computer Science","acronym":"LICS-02","location":"Copenhagen, Denmark"},"container-title":["Proceedings 17th Annual IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8005\/22127\/01029824.pdf?arnumber=1029824","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T00:32:54Z","timestamp":1585009974000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1029824\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/lics.2002.1029824","relation":{},"subject":[]}}