{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:32:47Z","timestamp":1725867167804},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319479576"},{"type":"electronic","value":"9783319479583"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47958-3_11","type":"book-chapter","created":{"date-parts":[[2016,10,8]],"date-time":"2016-10-08T09:40:52Z","timestamp":1475919652000},"page":"187-205","source":"Crossref","is-referenced-by-count":3,"title":["A Realizability Interpretation for Intersection and Union Types"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"de\u2019Liguoro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"Stolze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,9]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-54345-7_49","volume-title":"Mathematical Foundations of Computer Science 1991","author":"F Alessi","year":"1991","unstructured":"Alessi, F., Barbanera, F.: Strong conjunction and intersection types. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol. 520, pp. 64\u201373. Springer, Heidelberg (1991). doi: 10.1007\/3-540-54345-7_49"},{"key":"11_CR2","unstructured":"The Agda Programming Language (2016). http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php . Accessed 2 Sept 2016"},{"key":"11_CR3","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, vol. 103 of Studies in Logic and the Foundations of Mathematics. revised edition (1984)"},{"issue":"4","key":"11_CR4","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48(4), 931\u2013940 (1983)","journal-title":"J. Symbolic Logic"},{"issue":"2","key":"11_CR5","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1006\/inco.1995.1086","volume":"119","author":"F Barbanera","year":"1995","unstructured":"Barbanera, F., Dezani-Ciancaglini, M., de\u2019Liguoro, U.: Intersection and union types: syntax and semantics. Inf. Comput. 119(2), 202\u2013230 (1995)","journal-title":"Inf. Comput."},{"key":"11_CR6","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF01203032","volume":"33","author":"F Barbanera","year":"1994","unstructured":"Barbanera, F., Martini, S.: Proof-functional connectives and realizability. Arch. Math. Logic 33, 189\u2013211 (1994)","journal-title":"Arch. Math. Logic"},{"issue":"4","key":"11_CR7","doi-asserted-by":"crossref","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 $$\\lambda $$ -calculus. Notre Dame J. Formal Logic 21(4), 685\u2013693 (1980)","journal-title":"Notre Dame J. Formal Logic"},{"issue":"1","key":"11_CR8","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(93)90086-9","volume":"121","author":"M Coppo","year":"1993","unstructured":"Coppo, M., Ferrari, A.: Type inference, abstract interpretation and strictness analysis. Theoret. Comput. Sci. 121(1), 113\u2013143 (1993)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"11_CR9","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1016\/S1571-0661(04)00172-0","volume":"50","author":"B Capitani","year":"2001","unstructured":"Capitani, B., Loreti, M., Venneri, B.: Hyperformulae, parallel deductions and intersection types. Electr. Notes Theor. Comput. Sci. 50(2), 180\u2013198 (2001)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"11_CR10","unstructured":"The Coq Proof Assistant (2016). https:\/\/coq.inria.fr\/ . Accessed 2 Sept 2016"},{"issue":"2","key":"11_CR11","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1305\/ndjfl\/1039724889","volume":"38","author":"M Dezani-Ciancaglini","year":"1997","unstructured":"Dezani-Ciancaglini, M., Ghilezan, S., Venneri, B.: The relevance of intersection and union types. Notre Dame J. Formal Logic 38(2), 246\u2013269 (1997)","journal-title":"Notre Dame J. Formal Logic"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-17511-4_11","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"DJ Dougherty","year":"2010","unstructured":"Dougherty, D.J., Liquori, L.: Logic and computation in a lambda calculus with intersection and union types. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 173\u2013191. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_11"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Dunfield, J.: Elaborating intersection and union types. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, pp. 17\u201328. ACM (2012)","DOI":"10.1145\/2364527.2364534"},{"key":"11_CR14","unstructured":"The Epigram Programming Language (2016). https:\/\/code.google.com\/archive\/p\/epigram\/ . Accessed 2 Sept 2016"},{"issue":"1","key":"11_CR15","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"11_CR16","unstructured":"The Idris Programming Language (2016). http:\/\/www.idris-lang.org\/ . Accessed 2 Sept 2016"},{"key":"11_CR17","unstructured":"The Isabelle Proof Assistant (2016). https:\/\/isabelle.in.tum.de\/ . Accessed 2 Sept 2016"},{"key":"11_CR18","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0075313","volume-title":"Methods in Mathematical Logic","author":"EGK Lopez-Escobar","year":"1985","unstructured":"Lopez-Escobar, E.G.K.: Proof functional connectives. In: Prisco, C.A. (ed.) Methods in Mathematical Logic. LNM, vol. 1130, pp. 208\u2013221. Springer, Heidelberg (1985). doi: 10.1007\/BFb0075313"},{"issue":"205","key":"11_CR19","doi-asserted-by":"crossref","first-page":"1371","DOI":"10.1016\/j.ic.2007.03.005","volume":"9","author":"L Liquori","year":"2007","unstructured":"Liquori, L., Della Rocca, S.R.: Intersection typed system \u00e0 la Church. Inf. Comput. 9(205), 1371\u20131386 (2007)","journal-title":"Inf. Comput."},{"issue":"3","key":"11_CR20","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1305\/ndjfl\/1093635158","volume":"30","author":"G Mints","year":"1989","unstructured":"Mints, G.: The completeness of provable realizability. Notre Dame J. Formal Logic 30(3), 420\u2013441 (1989)","journal-title":"Notre Dame J. Formal Logic"},{"key":"11_CR21","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/S0019-9958(86)80019-5","volume":"71","author":"D MacQueen","year":"1986","unstructured":"MacQueen, D., Plotkin, G., Sethi, R.: An ideal model for recursive polymorphic types. Inf. Control 71, 95\u2013130 (1986)","journal-title":"Inf. Control"},{"key":"11_CR22","first-page":"407","volume":"15","author":"RK Meyer","year":"1972","unstructured":"Meyer, R.K., Routley, R.: Algebraic analysis of entailment I. Logique et Anal. 15, 407\u2013428 (1972)","journal-title":"Logique et Anal."},{"key":"11_CR23","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"11_CR24","unstructured":"Pottinger, G.: A type assignment for the strongly normalizable $$\\lambda $$ -terms. In: To Curry, H.B. (ed.) Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561\u2013577. Academic Press (1980)"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Prawitz, D.: Ideas and results in proof theory. In: Proceedings of the Second Scandinavian Logic Symposium, North-Holland (1971)","DOI":"10.1016\/S0049-237X(08)70849-8"},{"issue":"2","key":"11_CR26","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1017\/S0956796800001040","volume":"4","author":"BC Pierce","year":"1994","unstructured":"Pierce, B.C., Turner, D.N.: Simple type-theoretic foundations for object-oriented programming. J. Funct. Programm. 4(2), 207\u2013247 (1994)","journal-title":"J. Funct. Programm."},{"key":"11_CR27","series-title":"Progress in Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-1-4612-4118-8_9","volume-title":"Algol-like Languages","author":"JC Reynolds","year":"1997","unstructured":"Reynolds, J.C.: Design of the programming language Forsythe. Algol-like Languages. Progress in Theoretical Computer Science, pp. 173\u2013233. Birkh\u00e4user, Boston (1997)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, New York (1998)","DOI":"10.1017\/CBO9780511626364"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Della Rocca, S.R.: Intersection typed lambda-calculus. Electr. Notes. Theor. Comput. Sci. 70(1), 163\u2013181 (2003)","DOI":"10.1016\/S1571-0661(04)80496-1"},{"issue":"3","key":"11_CR30","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1017\/S0956796801004245","volume":"12","author":"JB Wells","year":"2002","unstructured":"Wells, J.B., Dimock, A., Muller, R., Turbak, F.: A calculus with polymorphic and polyvariant flow types. J. Funct. Program. 12(3), 183\u2013227 (2002)","journal-title":"J. Funct. Program."},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-45927-8_9","volume-title":"Programming Languages and Systems","author":"JB Wells","year":"2002","unstructured":"Wells, J.B., Haack, C.: Branching types. In: M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 115\u2013132. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45927-8_9"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47958-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:40:32Z","timestamp":1498336832000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47958-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319479576","9783319479583"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47958-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}