{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:45Z","timestamp":1761611205296},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_29","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:15:38Z","timestamp":1180656938000},"page":"414-429","source":"Crossref","is-referenced-by-count":7,"title":["Intersection Logic"],"prefix":"10.1007","author":[{"given":"Simona Ronchi","family":"Della Rocca","sequence":"first","affiliation":[]},{"given":"Luca","family":"Roversi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"issue":"1\u20132","key":"29_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","volume":"51","author":"S. Abramsky","year":"1991","unstructured":"Samson Abramsky. Domain theory in logical form. Ann. Pure Appl. Logic, 51(1\u20132):1\u201377, 1991.","journal-title":"Ann. Pure Appl. Logic"},{"key":"29_CR2","series-title":"Lect Notes Comput Sci","volume-title":"16h International Symposium on Mathematical Foundation of Computer Science (MFCS91)","author":"F. Alessi","year":"1991","unstructured":"F. Alessi and F. Barbanera. Strong conjunction and intersection types. In 16h International Symposium on Mathematical Foundation of Computer Science (MFCS91), volume Lecture Notes in Computer Science 520. Springer-Verlag, 1991."},{"key":"29_CR3","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01203032","volume":"33","author":"F. Barbanera","year":"1994","unstructured":"F. Barbanera and S. Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, 33:189\u2013211, 1994.","journal-title":"Archive for Mathematical Logic"},{"issue":"4","key":"29_CR4","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. Barendregt","year":"1984","unstructured":"Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symbolic Logic, 48(4):931\u2013940 (1984), 1983.","journal-title":"J. Symbolic Logic"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"B. Capitani, M. Loreti, and Venneri B. Hyperformulae, parallel deductions and intersection types. To appear in \u201cWorkshop on Bohm Theorem\u201d, IC ALP 2001, Creta (Greece), 2001.","DOI":"10.1016\/S1571-0661(04)00172-0"},{"issue":"4","key":"29_CR6","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the \u03bb-calculus. Notre Dame J. Formal Logic, 21(4):685\u2013693, 1980.","journal-title":"Notre Dame J. Formal Logic"},{"key":"29_CR7","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/S0049-237X(08)71819-6","volume-title":"Logic colloquium\u2019 82 (Florence, 1982)","author":"M. Coppo","year":"1984","unstructured":"Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. Extended type structures and filter lambda models. In Logic colloquium\u2019 82 (Florence, 1982), pages 241\u2013262. North-Holland, Amsterdam, 1984."},{"key":"29_CR8","unstructured":"H. Curry, R. Feys, and W. Craig. Combinatory Logic, volume 1. North Holland, 1958."},{"issue":"2","key":"29_CR9","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1305\/ndjfl\/1039724889","volume":"38","author":"M. Dezani-Ciancaglini","year":"1997","unstructured":"M. Dezani-Ciancaglini, S. Ghilezan, and B. Venneri. The \u201crelevance\u201d of intersection and union types. Notre Dame J. Formal Logic, 38(2):246\u2013269, 1997.","journal-title":"Notre Dame J. Formal Logic"},{"issue":"2","key":"29_CR10","first-page":"149","volume":"16","author":"L. Egidi","year":"1992","unstructured":"Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. Fund. Inform., 16(2):149\u2013169, 1992. Mathematical foundations of computer science\u2019 91 (Kazimierz Dolny, 1991).","journal-title":"Fund. Inform."},{"key":"29_CR11","volume-title":"Internal Report","author":"J.-Y. Girard","year":"2001","unstructured":"Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Internal Report, IML, Marseille, 2001."},{"key":"29_CR12","unstructured":"J.Y. Girard. Interpretation Fonctionelle et Elimination des Coupures de l\u2019Arithmetique d\u2019Ordre Superieur. PhD thesis, Universit\u00e9 Paris VII, 1972."},{"issue":"1\u20132","key":"29_CR13","first-page":"235","volume":"28","author":"J. R. Hindley","year":"1984","unstructured":"J. Roger Hindley. Coppo Dezani types do not correspond to propositional logic. Theoret. Comput. Sci., 28(1\u20132):235\u2013236, 1984.","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR14","unstructured":"Furio Honsell and Simona Ronchi Della Rocca. Reasoning about interpretations in qualitative lambda-models. In Programming Concepts and Methods, pages 505\u2013522. North Holland, 1990."},{"issue":"1","key":"29_CR15","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(92)90040-P","volume":"45","author":"F. Honsell","year":"1992","unstructured":"Furio Honsell and Simona Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. J. Comput. System Sci., 45(1):49\u201375, 1992.","journal-title":"J. Comput. System Sci."},{"key":"29_CR16","first-page":"241","volume-title":"Logic Algebra and Computer Science","author":"A. Kfoury","year":"1999","unstructured":"Assaf Kfoury. Beta-reduction as unification. In Logic Algebra and Computer Science, pages 241\u2013262. Polish Academy of Science, Warsaw, 1999."},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Daniel Leivant. Polymorphic type inference. Symposium on Principles of Programming Languages, 1983.","DOI":"10.1145\/567067.567077"},{"issue":"3","key":"29_CR18","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1305\/ndjfl\/1093635158","volume":"30","author":"G. E. Mints","year":"1989","unstructured":"G. E. Mints. The completeness of provable realizability. Notre Dame J. Formal Logic, 30(3):420\u2013441, 1989.","journal-title":"Notre Dame J. Formal Logic"},{"key":"29_CR19","first-page":"561","volume-title":"To H. B. Curry: essays on combinatory logic, lambda calculus and formalism","author":"G. Pottinger","year":"1980","unstructured":"Garrel Pottinger. A type assignment for the strongly normalizable \u03bb-terms. In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 561\u2013577. Academic Press, London, 1980."},{"key":"29_CR20","unstructured":"Dag Prawitz. Natural Deduction. Almquist & Wiksell."},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Design of the programming language Forsythe. In P. O\u2019Hearn and R.D. Tennent, editors, Algol-like Languages. Birkhauser, 1996.","DOI":"10.1007\/978-1-4612-4118-8_9"},{"key":"29_CR22","series-title":"Lect Notes Comput Sci","first-page":"399","volume-title":"Fifth Annual Conference of the EACSL (CSL\u2019 96)","author":"L. Roversi","year":"1996","unstructured":"L. Roversi. a Type-Free Resource-Aware \u03bb-Calculus. In Fifth Annual Conference of the EACSL (CSL\u2019 96), volume 1258 of Lecture Notes in Computer Science, pages 399\u2013413, Utrecht (The Nederland), September 1996. Springer-Verlag."},{"issue":"2","key":"29_CR23","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1093\/logcom\/4.2.109","volume":"4","author":"B. Venneri","year":"1994","unstructured":"Betti Venneri. Intersection types as logical formulae. J. Logic Comput., 4(2):109\u2013124, 1994.","journal-title":"J. Logic Comput."},{"key":"29_CR24","doi-asserted-by":"crossref","unstructured":"J. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A typed intermediate language for flow-directed compilation. In 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT97), pages 757\u2013771.","DOI":"10.1007\/BFb0030639"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:21:05Z","timestamp":1556450465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}