{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:03:53Z","timestamp":1725865433126},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"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-46750-4_11","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T02:11:57Z","timestamp":1474423917000},"page":"179-195","source":"Crossref","is-referenced-by-count":0,"title":["Unification for $$\\lambda $$ -calculi Without Propagation Rules"],"prefix":"10.1007","author":[{"given":"Fl\u00e1vio L. C.","family":"de Moura","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. J. Funct. Program. 1(4), 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"11_CR2","unstructured":"Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: Tiwari [36], pp. 6\u201321"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, 1\u20133 September 2014, pp. 363\u2013376. ACM (2014)","DOI":"10.1145\/2692915.2628154"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 659\u2013670. ACM (2014)","DOI":"10.1145\/2535838.2535886"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-15205-4_30","volume-title":"Computer Science Logic","author":"B Accattoli","year":"2010","unstructured":"Accattoli, B., Kesner, D.: The structural $$\\lambda $$ -calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381\u2013395. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15205-4_30"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-28717-6_5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Accattoli","year":"2012","unstructured":"Accattoli, B., Kesner, D.: The permutative $$\\lambda $$ -calculus. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 23\u201336. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_5"},{"issue":"1","key":"11_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-8(1:28)2012","volume":"8","author":"B Accattoli","year":"2012","unstructured":"Accattoli, B., Kesner, D.: Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods Comput. Sci. 8(1), 1\u201344 (2012)","journal-title":"Logical Methods Comput. Sci."},{"key":"11_CR8","unstructured":"Accattoli, B., Dal Lago, U.: On the invariance of the unitary cost model for head reduction. In: Tiwari [36], pp. 22\u201337"},{"issue":"4","key":"11_CR9","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1093\/jigpal\/9.4.489","volume":"9","author":"M Ayala-Rinc\u00f3n","year":"2001","unstructured":"Ayala-Rinc\u00f3n, M., Kamareddine, F.: Unification via the $$\\lambda s_e$$ -style of explicit substitution. Logical J. IGPL 9(4), 489\u2013523 (2001)","journal-title":"Logical J. IGPL"},{"key":"11_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.21711\/231766362003\/rmc241","volume":"24","author":"M Ayala-Rinc\u00f3n","year":"2003","unstructured":"Ayala-Rinc\u00f3n, M., Kamareddine, F.: On applying the $$\\lambda s_e$$ -style of unification for simply-typed higher order unification in the pure lambda calculus. Matem\u00e1tica Contempor\u00e2nea 24, 1\u201322 (2003)","journal-title":"Matem\u00e1tica Contempor\u00e2nea"},{"key":"11_CR11","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"391","volume-title":"34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)","author":"FLC Moura de","year":"2014","unstructured":"de Moura, F.L.C., Kesner, D., Ayala-Rinc\u00f3n, M.: Metaconfluence of calculi with explicit substitutions at a distance. In: Raman, V., Suresh, S.P. (eds.) 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), vol. 29, pp. 391\u2013402. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2014)"},{"key":"11_CR12","unstructured":"de Moura, F.L.C.: Higher-order unification via explicit substitutions at a distance. In: LSFA 2014 (2014). Accepted for short presentation"},{"issue":"1","key":"11_CR13","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/j.jal.2006.10.001","volume":"6","author":"FLC Moura de","year":"2008","unstructured":"de Moura, F.L.C., Ayala-Rinc\u00f3n, M., Kamareddine, F.: Higher-order unification: a structural relation between Huet\u2019s method and the one based on explicit substitutions. J. Appl. Logic 6(1), 72\u2013108 (2008)","journal-title":"J. Appl. Logic"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-32275-7_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"FLC Moura de","year":"2005","unstructured":"de Moura, F.L.C., Kamareddine, F., Ayala-Rinc\u00f3n, M.: Second-order matching via explicit substitutions. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 433\u2013448. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-32275-7_29"},{"issue":"2","key":"11_CR15","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0304-3975(93)90075-5","volume":"114","author":"DJ Dougherty","year":"1993","unstructured":"Dougherty, D.J.: Higher-order unification via combinators. TCS 114(2), 273\u2013298 (1993)","journal-title":"TCS"},{"key":"11_CR16","first-page":"135","volume":"69","author":"G Dowek","year":"1994","unstructured":"Dowek, G.: Third order matching is decidable. APAL 69, 135\u2013155 (1994)","journal-title":"APAL"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1009\u20131062. MIT press and Elsevier (2001). Chap. 16","DOI":"10.1016\/B978-044450813-3\/50018-7"},{"issue":"1\u20132","key":"11_CR18","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G Dowek","year":"2000","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher order unification via explicit substitutions. Inf. Comput. 157(1\u20132), 183\u2013235 (2000)","journal-title":"Inf. Comput."},{"issue":"5","key":"11_CR19","first-page":"699","volume":"6","author":"D Briaud","year":"1996","unstructured":"Briaud, D., Lescanne, P., Rouyer-Degli, J.: $$\\lambda \\upsilon $$ , a calculus of explicit substitutions which preserves strong normalization. JFP 6(5), 699\u2013722 (1996)","journal-title":"JFP"},{"key":"11_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"11_CR21","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W Goldfarb","year":"1981","unstructured":"Goldfarb, W.: The undecidability of the second-order unification problem. Theoret. Comput. Sci. 13(2), 225\u2013230 (1981)","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"11_CR22","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1017\/S0956796800003695","volume":"10","author":"B Guillaume","year":"2000","unstructured":"Guillaume, B.: The $$\\lambda s_e$$ -calculus does not preserve strong normalization. J. Func. Program. 10(4), 321\u2013325 (2000)","journal-title":"J. Func. Program."},{"issue":"3","key":"11_CR23","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G Huet","year":"1973","unstructured":"Huet, G.: The undecidability of unification in third order logic. Inf. Control 22(3), 257\u2013267 (1973)","journal-title":"Inf. Control"},{"issue":"1","key":"11_CR24","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed lambda-calculus. TCS 1(1), 27\u201357 (1975)","journal-title":"TCS"},{"key":"11_CR25","unstructured":"Huet, G.: R\u00e9solution d\u2019\u00e9quations dans les langages d\u2019ordre 1,2,.., $$\\omega $$ . Ph.D. thesis, University Paris-7 (1976)"},{"key":"11_CR26","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1017\/S0956796897002785","volume":"7","author":"F Kamareddine","year":"1997","unstructured":"Kamareddine, F., R\u00edos, A.: Extending a $$\\lambda $$ -calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. J. Func. Program. 7, 395\u2013420 (1997)","journal-title":"J. Func. Program."},{"issue":"31","key":"11_CR27","first-page":"1","volume":"5","author":"D Kesner","year":"2009","unstructured":"Kesner, D.: A theory of explicit substitutions with safe and full composition. Logical Methods Comput. Sci. 5(31), 1\u201329 (2009)","journal-title":"Logical Methods Comput. Sci."},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-16780-3_82","volume-title":"8th International Conference on Automated Deduction","author":"RD Lins","year":"1986","unstructured":"Lins, R.D.: A new formula for the execution of categorical combinators. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 89\u201398. Springer, Heidelberg (1986). doi: 10.1007\/3-540-16780-3_82"},{"issue":"1","key":"11_CR29","first-page":"51","volume":"11","author":"R Loader","year":"2003","unstructured":"Loader, R.: Higher order $$\\beta $$ matching is undecidable. Logic J. Interest Group Pure Appl. Logics 11(1), 51\u201368 (2003)","journal-title":"Logic J. Interest Group Pure Appl. Logics"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"Typed Lambda Calculi and Applications","author":"P-A Mellies","year":"1995","unstructured":"Mellies, P.-A.: Typed $$\\lambda $$ -calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 328\u2013334. Springer, Heidelberg (1995). doi: 10.1007\/BFb0014062"},{"issue":"3","key":"11_CR31","first-page":"65","volume":"175","author":"R Milner","year":"2007","unstructured":"Milner, R.: Local bigraphs and confluence: two conjectures: (extended abstract). ENTCS 175(3), 65\u201373 (2007)","journal-title":"ENTCS"},{"issue":"3","key":"11_CR32","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1017\/S0960129500003108","volume":"10","author":"V Padovani","year":"2000","unstructured":"Padovani, V.: Decidability of fourth-order matching. Math. Struct. Comput. Sci. 10(3), 361\u2013372 (2000)","journal-title":"Math. Struct. Comput. Sci."},{"key":"11_CR33","unstructured":"Renaud, F.: Metaconfluence of $${\\lambda }\\mathtt{j}$$ : dealing with non-deterministic replacements (2011). http:\/\/www.pps.univ-paris-diderot.fr\/~renaud\/lambdaj_mconf.pdf"},{"issue":"1\/2","key":"11_CR34","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W Snyder","year":"1989","unstructured":"Snyder, W., Gallier, J.H.: Higher-order unification revisited: complete sets of transformations. J. Symb. Comput. 8(1\/2), 101\u2013140 (1989)","journal-title":"J. Symb. Comput."},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11787006_30","volume-title":"Automata, Languages and Programming","author":"C Stirling","year":"2006","unstructured":"Stirling, C.: A game-theoretic approach to deciding higher-order matching. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 348\u2013359. Springer, Heidelberg (2006). doi: 10.1007\/11787006_30"},{"key":"11_CR36","unstructured":"Tiwari, A. (ed.) 23rd International Conference on Rewriting Techniques and Applications (RTA 2012). LIPIcs, Nagoya, Japan, 28 May 2012 \u2013 2 June 2012, vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,8]],"date-time":"2022-07-08T22:11:40Z","timestamp":1657318300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}