{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:21:00Z","timestamp":1742912460789,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031617157"},{"type":"electronic","value":"9783031617164"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-61716-4_2","type":"book-chapter","created":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:47:52Z","timestamp":1716954472000},"page":"17-35","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["YACC: Yet Another Church Calculus"],"prefix":"10.1007","author":[{"given":"Franco","family":"Barbanera","sequence":"first","affiliation":[]},{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[]},{"given":"Ugo","family":"de\u2019Liguoro","sequence":"additional","affiliation":[]},{"given":"Betti","family":"Venneri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,5,22]]},"reference":[{"key":"2_CR1","volume-title":"Entailment: The Logic of Relevance and Necessity","author":"AR Anderson","year":"1975","unstructured":"Anderson, A.R., Belnap, N.: Entailment: The Logic of Relevance and Necessity, vol. I. Princeton University Press, Princeton (1975)"},{"doi-asserted-by":"publisher","unstructured":"Alessi, F., Barbanera, F.: Strong conjunction and intersection types. In: Tarlecki, A. (ed.) MFCS. LNCS, vol.\u00a0520, pp. 64\u201373. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54345-7_49","key":"2_CR2","DOI":"10.1007\/3-540-54345-7_49"},{"doi-asserted-by":"publisher","unstructured":"van Bakel, S.: Strict intersection types for the lambda calculus. ACM Comput. Surv. 43(3), 20:1\u201320:49 (2011). https:\/\/doi.org\/10.1145\/1922649.1922657","key":"2_CR3","DOI":"10.1145\/1922649.1922657"},{"issue":"3","key":"2_CR4","doi-asserted-by":"publisher","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(3), 189\u2013211 (1994). https:\/\/doi.org\/10.1007\/BF01203032","journal-title":"Arch. Math. Logic"},{"unstructured":"Barendregt, H.: The lambda calculus, its syntax and semantics. In: Studies in logic and foundations of mathematics, vol.\u00a0103. North-Holland (1981)","key":"2_CR5"},{"issue":"4","key":"2_CR6","doi-asserted-by":"publisher","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. Symb. Logic 48(4), 931\u2013940 (1983). https:\/\/doi.org\/10.2307\/2273659","journal-title":"J. Symb. Logic"},{"doi-asserted-by":"publisher","unstructured":"Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press, Cambridge (2013). https:\/\/doi.org\/10.1017\/CBO9781139032636","key":"2_CR7","DOI":"10.1017\/CBO9781139032636"},{"doi-asserted-by":"publisher","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2: Background: Computational Structures, pp. 117\u2013309. Oxford University Press, Oxford (1992). https:\/\/doi.org\/10.1093\/oso\/9780198537618.003.0002","key":"2_CR8","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"doi-asserted-by":"publisher","unstructured":"Bernadet, A., Lengrand, S.: Complexity of strongly normalising $$\\lambda $$-terms via non-idempotent intersection types. In: Hofmann, M. (ed.) FOSSACS. LNCS, vol.\u00a06604, pp. 88\u2013107. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_7","key":"2_CR9","DOI":"10.1007\/978-3-642-19805-2_7"},{"unstructured":"Blaauwbroek, L.: On the interaction between unrestricted union and intersection types and computational effects. Master\u2019s thesis, Eindhoven University of Technology (2017). https:\/\/pure.tue.nl\/ws\/portalfiles\/portal\/88387896\/Masters_Thesis_Lasse_Blaauwbroek.pdf","key":"2_CR10"},{"doi-asserted-by":"publisher","unstructured":"Bono, V., Dezani-Ciancaglini, M.: A tale of intersection types. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS, pp. 7\u201320. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394733","key":"2_CR11","DOI":"10.1145\/3373718.3394733"},{"issue":"1\u20133","key":"2_CR12","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.tcs.2008.01.046","volume":"398","author":"V Bono","year":"2008","unstructured":"Bono, V., Venneri, B., Bettini, L.: A typed lambda calculus with intersection types. Theor. Comput. Sci. 398(1\u20133), 95\u2013113 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2008.01.046","journal-title":"Theor. Comput. Sci."},{"unstructured":"de\u00a0Carvalho, D.: Execution time of lambda-terms via denotational semantics and intersection types. CoRR abs\/0905.4251 (2009). http:\/\/arxiv.org\/abs\/0905.4251","key":"2_CR13"},{"issue":"2","key":"2_CR14","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5(2), 56\u201368 (1940). https:\/\/doi.org\/10.2307\/2266170","journal-title":"J. Symb. Logic"},{"issue":"4","key":"2_CR15","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 $$\\lambda $$-calculus. Notre Dame J. Formal Logic 21(4), 685\u2013693 (1980). https:\/\/doi.org\/10.1305\/ndjfl\/1093883253","journal-title":"Notre Dame J. Formal Logic"},{"unstructured":"Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Principal type schemes and lambda-calculus semantics. In: Hindley, R., Seldin, J.P. (eds.) To H.B.Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pp. 535\u2013560. Academic Press (1980)","key":"2_CR16"},{"issue":"1","key":"2_CR17","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1137\/0205036","volume":"27","author":"M Coppo","year":"1981","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms. Zeitschrift f\u00fcr Mathematishche Logik und Grundlagen der Mathematik 27(1), 45\u201358 (1981). https:\/\/doi.org\/10.1137\/0205036","journal-title":"Zeitschrift f\u00fcr Mathematishche Logik und Grundlagen der Mathematik"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"HB Curry","year":"1934","unstructured":"Curry, H.B.: Functionality in combinatory logic. Proc. Natl. Acad. Sci. USA 20, 584\u2013590 (1934). https:\/\/doi.org\/10.1073\/pnas.20.11.584","journal-title":"Proc. Natl. Acad. Sci. USA"},{"unstructured":"De\u00a0Benedetti, E., Ronchi Della\u00a0Rocca, S.: A type assignment for lambda-calculus complete both for FPTIME and strong normalization. CoRR abs\/1410.6298 (2014). http:\/\/arxiv.org\/abs\/1410.6298","key":"2_CR19"},{"issue":"3","key":"2_CR20","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1093\/logcom\/11.3.395","volume":"11","author":"M Dezani-Ciancaglini","year":"2001","unstructured":"Dezani-Ciancaglini, M., Honsell, F., Motohama, Y.: Approximation theorems for intersection type systems. J. Log. Comput. 11(3), 395\u2013417 (2001). https:\/\/doi.org\/10.1093\/logcom\/11.3.395","journal-title":"J. Log. Comput."},{"doi-asserted-by":"publisher","unstructured":"Dudenhefner, A., Rehof, J.: Intersection type calculi of bounded dimension. In: Castagna, G., Gordon, A.D. (eds.) POPL, pp. 653\u2013665. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009862","key":"2_CR21","DOI":"10.1145\/3009837.3009862"},{"doi-asserted-by":"publisher","unstructured":"Dudenhefner, A., Rehof, J.: Typability in bounded dimension. In: Ouaknine, J. (ed.) LICS, pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005127","key":"2_CR22","DOI":"10.1109\/LICS.2017.8005127"},{"doi-asserted-by":"publisher","unstructured":"Liquori, L., Della\u00a0Rocca, S.R.: Intersection-types \u00e0 la Church. Inf. Comput. 205(9), 1371\u20131386 (2007). https:\/\/doi.org\/10.1016\/j.ic.2007.03.005","key":"2_CR23","DOI":"10.1016\/j.ic.2007.03.005"},{"doi-asserted-by":"publisher","unstructured":"Lopez-Escobar, E.G.K.: Proof functional connectives. In: Di\u00a0Prisco, C.A. (ed.) Methods in Mathematical Logic, pp. 208\u2013221. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/BFb0075313","key":"2_CR24","DOI":"10.1007\/BFb0075313"},{"issue":"1\u20134","key":"2_CR25","doi-asserted-by":"publisher","first-page":"253","DOI":"10.3233\/FI-2012-778","volume":"121","author":"E Pimentel","year":"2012","unstructured":"Pimentel, E., Ronchi Della Rocca, S., Roversi, L.: Intersection types from a proof-theoretic perspective. Fund. Inf. 121(1\u20134), 253\u2013274 (2012). https:\/\/doi.org\/10.3233\/FI-2012-778","journal-title":"Fund. Inf."},{"issue":"2","key":"2_CR26","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1093\/logcom\/4.2.109","volume":"4","author":"B Venneri","year":"1994","unstructured":"Venneri, B.: Intersection types as logical formulae. J. Log. Comput. 4(2), 109\u2013124 (1994). https:\/\/doi.org\/10.1093\/logcom\/4.2.109","journal-title":"J. Log. Comput."},{"doi-asserted-by":"publisher","unstructured":"Wells, J.B., Haack, C.: Branching types. In: M\u00e9tayer, D.L. (ed.) ESOP. LNCS, vol.\u00a02305, pp. 115\u2013132. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45927-8_9","key":"2_CR27","DOI":"10.1007\/3-540-45927-8_9"}],"container-title":["Lecture Notes in Computer Science","Logics and Type Systems in Theory and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61716-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,29]],"date-time":"2024-05-29T03:49:04Z","timestamp":1716954544000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61716-4_2"}},"subtitle":["A Birthday Present for Herman Inspired by His Supervisor Activity"],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031617157","9783031617164"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61716-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"22 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}