{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:48:44Z","timestamp":1764557324861},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642387081"},{"type":"electronic","value":"9783642387098"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44602-7_26","type":"book-chapter","created":{"date-parts":[[2014,8,22]],"date-time":"2014-08-22T21:18:40Z","timestamp":1408742320000},"page":"341-354","source":"Crossref","is-referenced-by-count":10,"title":["The Inhabitation Problem for Non-idempotent Intersection Types"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Bucciarelli","sequence":"first","affiliation":[]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[]},{"given":"Simona","family":"Ronchi Della Rocca","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, revised edn. North-Holland, Amsterdam (1984)"},{"key":"26_CR2","unstructured":"Ben-Yelles, C.: Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, University of Wales Swansea (1979)"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Bernadet, A., Lengrand, S.: Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science\u00a09(4) (2013)","DOI":"10.2168\/LMCS-9(4:3)2013"},{"key":"26_CR4","unstructured":"Bunder, M.W.: The inhabitation problem for intersection types. In: CATS. CRPIT, vol.\u00a077, pp. 7\u201314. Australian Computer Society (2008)"},{"key":"26_CR5","unstructured":"Carvalho, D.D.: S\u00e8mantique de la logique lin\u00e9aire et temps de calcul. PhD thesis, Universit\u00e9 de la Mediterran\u00e9e Aix-Marseille 2 (2007)"},{"issue":"4","key":"26_CR6","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the \u03bb-calculus. Notre Dame J. Form. Log.\u00a021(4), 685\u2013693 (1980)","journal-title":"Notre Dame J. Form. Log."},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"De Benedetti, E., Ronchi Della Rocca, S.: Bounding normalization time through intersection types. In: Proc. of ITRS 2012. EPTCS, pp. 48\u201357 (2013)","DOI":"10.4204\/EPTCS.121.4"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1016\/j.tcs.2008.01.023","volume":"398","author":"P. Gianantonio Di","year":"2008","unstructured":"Di Gianantonio, P., Honsell, F., Lenisa, M.: A type assignment system for game semantics. Theor. Comput. Sci.\u00a0398, 150\u2013169 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR9","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.tcs.2011.11.027","volume":"424","author":"T. Ehrhard","year":"2012","unstructured":"Ehrhard, T.: The Scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci.\u00a0424, 20\u201345 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR10","series-title":"Cambridge Tracts in Theoretical Comp. Scie","volume-title":"Basic Simple Type Theory","author":"J.R. Hindley","year":"2008","unstructured":"Hindley, J.R.: Basic Simple Type Theory. Cambridge Tracts in Theoretical Comp. Scie. Cambridge University Press, Amsterdam (2008)"},{"issue":"2","key":"26_CR11","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S0956796808007144","volume":"19","author":"C.B. Jay","year":"2009","unstructured":"Jay, C.B., Kesner, D.: First-class patterns. Journal of Functional Programming\u00a019(2), 191\u2013225 (2009)","journal-title":"Journal of Functional Programming"},{"key":"26_CR12","series-title":"LNCS","first-page":"296","volume-title":"TCS 2014","author":"D. Kesner","year":"2014","unstructured":"Kesner, D., Ventura, D.: Quantitative types for the linear substitution calculus. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol.\u00a08705, pp. 296\u2013310. Springer, Heidelberg (2014)"},{"issue":"3","key":"26_CR13","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1093\/logcom\/10.3.411","volume":"10","author":"A.J. Kfoury","year":"2000","unstructured":"Kfoury, A.J.: A Linearization of the Lambda-Calculus and Consequences. J. Logic Comp.\u00a010(3), 411\u2013436 (2000)","journal-title":"J. Logic Comp."},{"issue":"1-3","key":"26_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2003.10.032","volume":"311","author":"A.J. Kfoury","year":"2004","unstructured":"Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci.\u00a0311(1-3), 1\u201370 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR15","volume-title":"Lambda-Calculus, Types and Models","author":"J.L. Krivine","year":"1993","unstructured":"Krivine, J.L.: Lambda-Calculus, Types and Models. Ellis Horwood, Hemel Hempstead, Masson, Paris (1993)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BFb0014060","volume-title":"Typed Lambda Calculi and Applications","author":"T. Kurata","year":"1995","unstructured":"Kurata, T., Takahashi, M.: Decidable properties of intersection type systems. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 297\u2013311. Springer, Heidelberg (1995)"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Mairson, H., Neergaard, P.M.: Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In: Proc. of ICFP 2004, pp. 138\u2013149 (2004)","DOI":"10.1145\/1016848.1016871"},{"key":"26_CR18","doi-asserted-by":"crossref","first-page":"358","DOI":"10.3233\/FI-2010-324","volume":"103","author":"M. Pagani","year":"2010","unstructured":"Pagani, M., Ronchi Della Rocca, S.: Linearity, non-determinism and solvability. Fundamenta Informaticae\u00a0103, 358\u2013373 (2010)","journal-title":"Fundamenta Informaticae"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-642-12032-9_25","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Pagani","year":"2010","unstructured":"Pagani, M., della Rocca, S.R.: Solvability in resource lambda-calculus. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 358\u2013373. Springer, Heidelberg (2010)"},{"key":"26_CR20","unstructured":"Paolini, L., Piccolo, M., Ronchi Della Rocca, S.: Logical relational lambda-models. Accepted for publication in MSCS (2013)"},{"issue":"3","key":"26_CR21","doi-asserted-by":"publisher","first-page":"1195","DOI":"10.2307\/2586625","volume":"64","author":"P. Urzyczyn","year":"1999","unstructured":"Urzyczyn, P.: The emptiness problem for intersection types. Journal of Symbolic Logic\u00a064(3), 1195\u20131215 (1999)","journal-title":"Journal of Symbolic Logic"},{"key":"26_CR22","unstructured":"Urzyczyn, P.: personal communication (2014)"},{"key":"26_CR23","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","volume":"102","author":"S. Bakel van","year":"1992","unstructured":"van Bakel, S.: Complete restrictions of the intersection type discipline. Theor. Comput. Sci.\u00a0102, 135\u2013163 (1992)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Advanced Information Systems Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44602-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T12:39:34Z","timestamp":1598186374000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44602-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642387081","9783642387098"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44602-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}