{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T21:40:02Z","timestamp":1750110002410,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662544570"},{"type":"electronic","value":"9783662544587"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54458-7_27","type":"book-chapter","created":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T09:22:57Z","timestamp":1489569777000},"page":"461-479","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Lambda-Free Higher-Order Recursive\u00a0Path\u00a0Order"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Wand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,16]]},"reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-44881-0_27","volume-title":"Rewriting Techniques and Applications","author":"T Aoto","year":"2003","unstructured":"Aoto, T., Yamada, T.: Termination of simply typed term rewriting by translation and labelling. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 380\u2013394. Springer, Heidelberg (2003). doi:10.1007\/3-540-44881-0_27"},{"issue":"1\u20132","key":"27_CR2","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1\u20132), 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic, vol. 9, pp. 215\u2013254. Elsevier (2014)","DOI":"10.1016\/B978-0-444-51624-4.50005-8"},{"issue":"1","key":"27_CR5","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reasoning"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14052-5_11"},{"key":"27_CR7","unstructured":"Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of recursive path orders for lambda-free higher-order terms. Archive of Formal Proofs, formal proof development (2016). https:\/\/isa-afp.org\/entries\/Lambda_Free_RPOs.shtml"},{"key":"27_CR8","unstructured":"Blanchette, J.C., Waldmann, U., Wand, D.: A lambda-free higher-order recursive path order. Technical report (2016). http:\/\/people.mpi-inf.mpg.de\/jblanche\/lambda_free_rpo_rep.pdf"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/10721975_4","volume-title":"Rewriting Techniques and Applications","author":"F Blanqui","year":"2000","unstructured":"Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 47\u201361. Springer, Heidelberg (2000). doi:10.1007\/10721975_4"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Blanqui, F., Jouannaud, J., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4) (2015)","DOI":"10.2168\/LMCS-11(4:3)2015"},{"issue":"4","key":"27_CR11","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827\u2013859 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"27_CR12","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1093\/logcom\/exs027","volume":"23","author":"M Bofill","year":"2013","unstructured":"Bofill, M., Borralleras, C., Rodr\u00edguez-Carbonell, E., Rubio, A.: The recursive path and polynomial ordering for first-order and higher-order terms. J. Log. Comput. 23(1), 263\u2013305 (2013)","journal-title":"J. Log. Comput."},{"issue":"1","key":"27_CR13","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10817-011-9244-z","volume":"50","author":"M Bofill","year":"2013","unstructured":"Bofill, M., Rubio, A.: Paramodulation with non-monotonic orderings and simplification. J. Autom. Reasoning 50(1), 51\u201398 (2013)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"27_CR14","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-010-9211-0","volume":"49","author":"M Codish","year":"2012","unstructured":"Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: SAT solving for termination proofs with recursive path orders and dependency pairs. J. Autom. Reasoning 49(1), 53\u201393 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"27_CR15","unstructured":"Contejean, \u00c9., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schau\u00df, M. (ed.) Rewriting Techniques and Applications (RTA 2011). Leibniz International Proceedings in Informatics (LIPIcs), vol. 10, pp. 21\u201330. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2011)"},{"issue":"8","key":"27_CR16","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-27813-9_14"},{"issue":"2","key":"27_CR18","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81\u201391 (1950)","journal-title":"J. Symb. Log."},{"issue":"3","key":"27_CR19","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10817-012-9248-3","volume":"50","author":"N Hirokawa","year":"2013","unstructured":"Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination and complexity. J. Autom. Reasoning 50(3), 279\u2013315 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Huet, G., Oppen, D.C.: Equations and rewrite rules: A survey. In: Book, R.V. (ed.) Formal Language Theory: Perspectives and Open Problems, pp. 349\u2013405. Academic Press (1980)","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Hughes, R.J.M.: Super-combinators: A new implementation method for applicative languages. In: ACM Symposium on LISP and Functional Programming (LFP 1982), pp. 1\u201310. ACM Press (1982)","DOI":"10.1145\/800068.802129"},{"key":"27_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-61464-8_46","volume-title":"Rewriting Techniques and Applications","author":"J-P Jouannaud","year":"1996","unstructured":"Jouannaud, J.-P., Rubio, A.: A recursive path ordering for higher-order terms in $$\\eta $$-long $$\\beta $$-normal form. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 108\u2013122. Springer, Heidelberg (1996). doi:10.1007\/3-540-61464-8_46"},{"issue":"1","key":"27_CR23","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/1206035.1206037","volume":"54","author":"J Jouannaud","year":"2007","unstructured":"Jouannaud, J., Rubio, A.: Polymorphic higher-order recursive path orderings. J. ACM 54(1), 2:1\u20132:48 (2007)","journal-title":"J. ACM"},{"issue":"1","key":"27_CR24","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1006\/jsco.1996.0002","volume":"21","author":"R Kennaway","year":"1996","unstructured":"Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.: Comparing curried and uncurried rewriting. J. Symb. Comput. 21(1), 15\u201339 (1996)","journal-title":"J. Symb. Comput."},{"key":"27_CR25","unstructured":"Kop, C.: Higher Order Termination. Ph.D. thesis, Vrije Universiteit Amsterdam (2012)"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1007\/978-3-540-89439-1_48","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Kop","year":"2008","unstructured":"Kop, C., Raamsdonk, F.: A higher-order iterative path ordering. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 697\u2013711. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-89439-1_48"},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/BFb0055142","volume-title":"Theorem Proving in Higher Order Logics","author":"M Lifantsev","year":"1998","unstructured":"Lifantsev, M., Bachmair, L.: An LPO-based termination ordering for higher-order terms without $$\\lambda $$-abstraction. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 277\u2013293. Springer, Heidelberg (1998). doi:10.1007\/BFb0055142"},{"key":"27_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/3-540-59200-8_45","volume-title":"Rewriting Techniques and Applications","author":"O Lysne","year":"1995","unstructured":"Lysne, O., Piris, J.: A termination ordering for higher order rewrite systems. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 26\u201340. Springer, Heidelberg (1995). doi:10.1007\/3-540-59200-8_45"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Logic in Computer Science (LICS 1991), pp. 342\u2013349. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151658"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"27_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-24364-6_17","volume-title":"Frontiers of Combining Systems","author":"C Sternagel","year":"2011","unstructured":"Sternagel, C., Thiemann, R.: Generalized and formalized uncurrying. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 243\u2013258. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-24364-6_17"},{"key":"27_CR33","unstructured":"Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: Tiwari, A. (ed.) Rewriting Techniques and Applications (RTA 2012). LIPIcs, vol. 15, pp. 339\u2013354. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452\u2013468. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03359-9_31"},{"key":"27_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-25979-4_3","volume-title":"Rewriting Techniques and Applications","author":"Y Toyama","year":"2004","unstructured":"Toyama, Y.: Termination of S-expression rewriting systems: lexicographic path ordering for higher-order terms. In: Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 40\u201354. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-25979-4_3"},{"issue":"1","key":"27_CR36","first-page":"31","volume":"9","author":"DA Turner","year":"1979","unstructured":"Turner, D.A.: A new implementation technique for applicative languages. Softw.: Pract. Experience 9(1), 31\u201349 (1979)","journal-title":"Softw.: Pract. Experience"},{"key":"27_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-45127-7_25","volume-title":"Rewriting Techniques and Applications","author":"T Yamada","year":"2001","unstructured":"Yamada, T.: Confluence and termination of simply typed term rewriting systems. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 338\u2013352. Springer, Heidelberg (2001). doi:10.1007\/3-540-45127-7_25"},{"key":"27_CR38","unstructured":"Zantema, H.: Termination. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181\u2013259. Cambridge University Press (2003)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54458-7_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T21:23:18Z","timestamp":1750108998000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54458-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544570","9783662544587"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54458-7_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}