{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:04:04Z","timestamp":1743069844052,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452308"},{"type":"electronic","value":"9783030452315"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Intersection types are an essential tool in the analysis of operational and denotational properties of lambda-terms and functional programs. Among them, non-idempotent intersection types provide precise quantitative information about the evaluation of terms and programs. However, unlike simple or second-order types, intersection types cannot be considered as a logical system because the application rule (or the intersection rule, depending on the presentation of the system) involves a condition stipulating that the proofs of premises must have the same structure. Using earlier work introducing an indexed version of Linear Logic, we show that non-idempotent typing can be given a logical form in a system where formulas represent hereditarily indexed families of intersection types.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_11","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"198-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Non-idempotent Intersection Types in Logical Form"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5231-5504","authenticated-orcid":false,"given":"Thomas","family":"Ehrhard","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"11_CR1","unstructured":"F.\u00a0Breuvart, G.\u00a0Manzonetto, and D.\u00a0Ruoppolo. Relational graph models at work. Logical Methods in Computer Science, 14(3), 2018."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bucciarelli and T.\u00a0Ehrhard. On phase semantics and denotational semantics in multiplicative-additive linear logic. Annals of Pure and Applied Logic, 102(3):247\u2013282, 2000.","DOI":"10.1016\/S0168-0072(99)00040-8"},{"key":"11_CR3","unstructured":"A.\u00a0Bucciarelli and T.\u00a0Ehrhard. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, 109(3):205\u2013241, 2001."},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"M.\u00a0Coppo and M.\u00a0Dezani-Ciancaglini. An extension of the basic functionality theory for the $$\\lambda $$-calculus. Notre Dame Journal of Formal Logic, 21(4):685\u2013693, 1980.","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"M.\u00a0Coppo, M.\u00a0Dezani-Ciancaglini, and B.\u00a0Venneri. Functional characters of solvable terms. Mathematical Logic Quarterly, 27(2-6):45\u201358, 1981.","DOI":"10.1002\/malq.19810270205"},{"key":"11_CR6","unstructured":"D. de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs\/0905.4251, 2009."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"D.\u00a0de\u00a0Carvalho. Execution time of $$\\lambda $$-terms via denotational semantics and intersection types. MSCS, 28(7):1169\u20131203, 2018.","DOI":"10.1017\/S0960129516000396"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"T.\u00a0Ehrhard. The Scott model of linear logic is the extensional collapse of its relational model. Theoretical Computer Science, 424:20\u201345, 2012.","DOI":"10.1016\/j.tcs.2011.11.027"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"T.\u00a0Ehrhard and L.\u00a0Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2-3):347\u2013372, 2008.","DOI":"10.1016\/j.tcs.2008.06.001"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"T. S. Freeman and F. Pfenning. Refinement Types for ML. In D. S. Wise, editor, Proceedings of the ACM SIGPLAN\u201991 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, pages 268\u2013277. ACM, 1991.","DOI":"10.1145\/113446.113468"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Normal functors, power series and the $$\\lambda $$-calculus. Annals of Pure and Applied Logic, 37:129\u2013177, 1988.","DOI":"10.1016\/0168-0072(88)90025-5"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"J.\u00a0R. Hindley. Coppo-dezani types do not correspond to propositional logic. Theoretical Computer Science, 28:235\u2013236, 1984.","DOI":"10.1016\/0304-3975(83)90074-9"},{"key":"11_CR13","unstructured":"J.-L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood Series in Computers and Their Applications. Ellis Horwood, 1993. Translation by Ren\u00e9 Cori from French 1990 edition (Masson)."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"L.\u00a0Liquori and S.\u00a0R.\u00a0D. Rocca. Intersection-types \u00e0 la Church. Information and Computation, 205(9):1371\u20131386, 2007.","DOI":"10.1016\/j.ic.2007.03.005"},{"key":"11_CR15","unstructured":"L. Liquori and C. Stolze. The Delta-calculus: Syntax and Types. In H. Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany., volume 131 of LIPIcs, pages 28:1\u201328:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T13:32:57Z","timestamp":1610026377000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}