{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:12:48Z","timestamp":1725664368143},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581406"},{"type":"electronic","value":"9783540484424"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58140-5_33","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:19:35Z","timestamp":1330269575000},"page":"353-365","source":"Crossref","is-referenced-by-count":3,"title":["Comparing cubes"],"prefix":"10.1007","author":[{"given":"Steffen","family":"Bakel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simona Ronchi","family":"Rocca","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pawe\u0142","family":"Urzyczyn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Barendregt, H.P., Lambda Calculi with Types, Handbook of Logic in Computer Science, Abramsky, Gabbai, Maibaum eds., Oxford University Press, 1991.","key":"33_CR1","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"issue":"2","key":"33_CR2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H.P. Barendregt","year":"1991","unstructured":"Barendregt, H.P., Introduction to Generalised Type Systems, Journal of Functional Programming, volume 1(2), 125\u2013154, 1991.","journal-title":"Journal of Functional Programming"},{"key":"33_CR3","volume-title":"Towards a Mathematical Analysis of Type Dependence in Coquand-Huet Calculus of Constructions and the Other Systems in Barendregt's Cube","author":"S. Berardi","year":"1988","unstructured":"Berardi, S., Towards a Mathematical Analysis of Type Dependence in Coquand-Huet Calculus of Constructions and the Other Systems in Barendregt's Cube, Department of Computer Science, CMU, and Dipartimento di Matematica, Torino, 1988."},{"doi-asserted-by":"crossref","unstructured":"Curry, H.B., Modified Basic Functionality in Combinatory Logic, Dialectica, 1969.","key":"33_CR4","DOI":"10.1111\/j.1746-8361.1969.tb01183.x"},{"unstructured":"Coquand, T., Metamathematical Investigations of a Calculus of Constructions, Logic and Computer Science, Odifreddi ed., Academic Press, 91\u2013122, 1990.","key":"33_CR5"},{"issue":"2","key":"33_CR6","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T. and Huet, G., The Calculus of Constructions, Information and Computation, 76(2,3), 95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"33_CR7","first-page":"139","volume":"664","author":"G. Dowek","year":"1993","unstructured":"Dowek, G., The Undecidability of Typability in the Lambda-Pi-Calculus, Proc. Typed Lambda Calculi and Applications, LNCS 664, 139\u2013145, 1993.","journal-title":"LNCS"},{"issue":"2","key":"33_CR8","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Geuvers, H. and Nederhof, M., Modular Proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming, 1(2), 155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"doi-asserted-by":"crossref","unstructured":"Giannini, P. and Ronchi Della Rocca, S., Characterization of Typings in Polymorphic Type Discipline, Proc. Logic in Computer Science, IEEE, 61\u201370, 1988.","key":"33_CR9","DOI":"10.1109\/LICS.1988.5101"},{"issue":"1","key":"33_CR10","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3233\/FI-1993-191-205","volume":"19","author":"P. Giannini","year":"1993","unstructured":"Giannini, P., Honsell, F. and Ronchi Della Rocca, S., Type Inference: Some Results, Some Problems, Fundamenta Informaticae, 19(1,2), pp.87\u2013126, 1993.","journal-title":"Fundamenta Informaticae"},{"key":"33_CR11","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y., The System F of Variable Types, Fifteen Years Later, Theoretical Computer Science, 45, 159\u2013192, 1987.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Harper, B., Honsell, F. and Plotkin, G., A Framework for Defining Logics, Journal of the ACM, 40, 1993.","key":"33_CR12","DOI":"10.1145\/138027.138060"},{"key":"33_CR13","volume-title":"PhD-thesis","author":"J. W. Klop","year":"1980","unstructured":"Klop, J. W., Combinatory Reduction Systems, PhD-thesis, Rijksuniversiteit Utrecht, 1980."},{"doi-asserted-by":"crossref","unstructured":"Leivant, D., Polymorphic Type Inference, In Symposium on Principles of Programming Languages, ACM, 88\u201398, 1983.","key":"33_CR14","DOI":"10.1145\/567067.567077"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C., Towards a Theory of Type Structures, Proc. Paris Colloquium on Programming, Springer Verlag, 408\u2013425, 1974.","key":"33_CR15","DOI":"10.1007\/3-540-06859-7_148"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58140-5_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T15:46:52Z","timestamp":1713628012000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58140-5_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581406","9783540484424"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-58140-5_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}