{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:54:34Z","timestamp":1781927674783,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T00:00:00Z","timestamp":1630886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,9,6]]},"DOI":"10.1145\/3479394.3479403","type":"proceedings-article","created":{"date-parts":[[2021,10,7]],"date-time":"2021-10-07T22:23:02Z","timestamp":1633645382000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories"],"prefix":"10.1145","author":[{"given":"Gaspard","family":"F\u00e9rey","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, \u00e9quipe INRIA Deducteam, Laboratoire de M\u00e9thodes Formelles, \u00c9cole Normale Sup\u00e9rieure de Paris-Saclay, 91190 Gif-sur-Yvette, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Pierre","family":"Jouannaud","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, \u00e9quipe INRIA Deducteam, Laboratoire de M\u00e9thodes Formelles, \u00c9cole Normale Sup\u00e9rieure de Paris-Saclay, 91190 Gif-sur-Yvette, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"HOR","author":"Assaf A.","year":"2016","unstructured":"A. Assaf , G. Dowek , J.-P. Jouannaud and J. Liu . 2018. Untyped Confluence in Dependent Type Theories. draft hal-01515505. INRIA . presented at HOR 2016 . A. Assaf, G. Dowek, J.-P. Jouannaud and J. Liu. 2018. Untyped Confluence in Dependent Type Theories. draft hal-01515505. INRIA. presented at HOR 2016."},{"key":"e_1_3_2_1_2_1","unstructured":"A. Assaf G. Burel R. Cauderlier G. Dowek C. Dubois F. Gilbert P. Halmagrand O. Hermant and R. Saillard. 2019. Dedukti: a Logical Framework based on the Lambda-Pi-Calculus Modulo Theory. draft. INRIA.  A. Assaf G. Burel R. Cauderlier G. Dowek C. Dubois F. Gilbert P. Halmagrand O. Hermant and R. Saillard. 2019. Dedukti: a Logical Framework based on the Lambda-Pi-Calculus Modulo Theory. draft. INRIA."},{"key":"e_1_3_2_1_3_1","volume-title":"International Conference, TYPES 2008","author":"Barras B.","year":"2008","unstructured":"B. Barras , P. Corbineau , B. Gr\u00e9goire , H. Herbelin , and J.\u00a0 L. Sacchini . 2008 . A New Elimination Rule for the Calculus of Inductive Constructions. In Types for Proofs and Programs , International Conference, TYPES 2008 , Torino, Italy , March 26-29, 2008, Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a05497), S.\u00a0Berardi, F.\u00a0Damiani, and U.\u00a0de\u2019Liguoro (Eds.). Springer, 32\u201348. https:\/\/doi.org\/10.1007\/978-3-642-02444-3_3 10.1007\/978-3-642-02444-3_3 B. Barras, P. Corbineau, B. Gr\u00e9goire, H. Herbelin, and J.\u00a0L. Sacchini. 2008. A New Elimination Rule for the Calculus of Inductive Constructions. In Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a05497), S.\u00a0Berardi, F.\u00a0Damiani, and U.\u00a0de\u2019Liguoro (Eds.). Springer, 32\u201348. https:\/\/doi.org\/10.1007\/978-3-642-02444-3_3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004426"},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. ACM Program. Lang. 5, POPL","author":"Cockx J.","year":"2021","unstructured":"J. Cockx , N. Tabareau , and T. Winterhalter . 2021. The taming of the rew: a type theory with computational assumptions . Proc. ACM Program. Lang. 5, POPL ( 2021 ), 1\u201329. https:\/\/doi.org\/10.1145\/3434341 10.1145\/3434341 J. Cockx, N. Tabareau, and T. Winterhalter. 2021. The taming of the rew: a type theory with computational assumptions. Proc. ACM Program. Lang. 5, POPL (2021), 1\u201329. https:\/\/doi.org\/10.1145\/3434341"},{"key":"e_1_3_2_1_7_1","volume-title":"HOR","author":"Dowek G.","year":"2016","unstructured":"G. Dowek , G. F\u00e9rey , J.-P. Jouannaud and J. Liu . 2021. Confluence of Left-Linear Higher-Order Rewrite Theories by Checking their Nested Critical Pairs. draft hal-03126111. INRIA . Presented at HOR 2016 . submitted to MSCS. G. Dowek, G. F\u00e9rey, J.-P. Jouannaud and J. Liu. 2021. Confluence of Left-Linear Higher-Order Rewrite Theories by Checking their Nested Critical Pairs. draft hal-03126111. INRIA. Presented at HOR 2016. submitted to MSCS."},{"key":"e_1_3_2_1_8_1","unstructured":"G. F\u00e9rey and J.-P. Jouannaud. 2021. Confluence in UnTyped Higher-Order Theories by Means of Critical Pairs. draft. hal-03126102. INRIA. Under revision for TOCL available from http:\/\/dedukti.gforge.inria.fr\/.  G. F\u00e9rey and J.-P. Jouannaud. 2021. Confluence in UnTyped Higher-Order Theories by Means of Critical Pairs. draft. hal-03126102. INRIA. Under revision for TOCL available from http:\/\/dedukti.gforge.inria.fr\/."},{"key":"e_1_3_2_1_9_1","volume-title":"International Workshop TYPES\u201994","author":"Goguen H.","year":"1994","unstructured":"H. Goguen . 1994 . The Metatheory of UTT. In Types for Proofs and Programs , International Workshop TYPES\u201994 , B\u00e5stad, Sweden , June 6-10, 1994, Selected Papers(Lecture Notes in Computer Science, Vol.\u00a0996), P.\u00a0Dybjer, B.\u00a0Nordstr\u00f6m, and J.\u00a0M. Smith(Eds.). Springer, 60\u201382. https:\/\/doi.org\/10.1007\/3-540-60579-7_4 10.1007\/3-540-60579-7_4 H. Goguen. 1994. The Metatheory of UTT. In Types for Proofs and Programs, International Workshop TYPES\u201994, B\u00e5stad, Sweden, June 6-10, 1994, Selected Papers(Lecture Notes in Computer Science, Vol.\u00a0996), P.\u00a0Dybjer, B.\u00a0Nordstr\u00f6m, and J.\u00a0M. Smith(Eds.). Springer, 60\u201382. https:\/\/doi.org\/10.1007\/3-540-60579-7_4"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.08.030"},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS \u201991)","author":"Jouannaud J.-P.","unstructured":"J.-P. Jouannaud and M. Okada . 1991. A computation model for executable higher-order algebraic specification languages . In Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS \u201991) . Amsterdam, The Netherlands, 350\u2013361. J.-P. Jouannaud and M. Okada. 1991. A computation model for executable higher-order algebraic specification languages. In Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS \u201991). Amsterdam, The Netherlands, 350\u2013361."},{"key":"e_1_3_2_1_12_1","volume-title":"Combinatory Reduction Systems. Number 127 in Mathematical Centre Tracts. CWI","author":"Klop W.","unstructured":"J.\u00a0 W. Klop . 1980. Combinatory Reduction Systems. Number 127 in Mathematical Centre Tracts. CWI , Amsterdam, The Netherlands. PhD Thesis . J.\u00a0W. Klop. 1980. Combinatory Reduction Systems. Number 127 in Mathematical Centre Tracts. CWI, Amsterdam, The Netherlands. PhD Thesis."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_20"},{"key":"e_1_3_2_1_14_1","volume-title":"Confluence of Layered Rewrite Systems. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015","author":"Liu J.","year":"2015","unstructured":"J. Liu , J.-P. Jouannaud , and M. Ogawa . 2015 . Confluence of Layered Rewrite Systems. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015 , September 7-10, 2015 , Berlin, Germany(LIPIcs, Vol.\u00a041), S.\u00a0Kreutzer (Ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 423\u2013440. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2015.423 10.4230\/LIPIcs.CSL.2015.423 J. Liu, J.-P. Jouannaud, and M. Ogawa. 2015. Confluence of Layered Rewrite Systems. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany(LIPIcs, Vol.\u00a041), S.\u00a0Kreutzer (Ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 423\u2013440. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2015.423"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"A. Middeldorp V. van Oostrom F. van Raamsdonk and R.\u00a0C. de Vrijer (Eds.). 2005. Processes Terms and Cycles: Steps on the Road to Infinity Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday. Lecture Notes in Computer Science Vol.\u00a03838. Springer.  A. Middeldorp V. van Oostrom F. van Raamsdonk and R.\u00a0C. de Vrijer (Eds.). 2005. Processes Terms and Cycles: Steps on the Road to Infinity Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday. Lecture Notes in Computer Science Vol.\u00a03838. Springer.","DOI":"10.1007\/11601548"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151658"},{"key":"#cr-split#-e_1_3_2_1_19_1.1","doi-asserted-by":"crossref","unstructured":"T. Nipkow L.\u00a0C. Paulson and M. Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science Vol.\u00a02283. Springer. https:\/\/doi.org\/10.1007\/3-540-45949-9 10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"#cr-split#-e_1_3_2_1_19_1.2","doi-asserted-by":"crossref","unstructured":"T. Nipkow L.\u00a0C. Paulson and M. Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science Vol.\u00a02283. Springer. https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the ACM-SIGSAM 1989 Symposium on Symbolic and Algebraic Computation, ISSAC \u201989","author":"Okada M.","year":"1989","unstructured":"M. Okada . 1989 . Strong Normalizability for the Combined System of the Typed lambda Calculus and an Arbitrary Convergent Term Rewrite System . In Proceedings of the ACM-SIGSAM 1989 Symposium on Symbolic and Algebraic Computation, ISSAC \u201989 , Portland, Oregon, USA , 1989, G.\u00a0H. Gonnet (Ed.). ACM, 357\u2013363. https:\/\/doi.org\/10.1145\/74540.74582 10.1145\/74540.74582 M. Okada. 1989. Strong Normalizability for the Combined System of the Typed lambda Calculus and an Arbitrary Convergent Term Rewrite System. In Proceedings of the ACM-SIGSAM 1989 Symposium on Symbolic and Algebraic Computation, ISSAC \u201989, Portland, Oregon, USA, 1989, G.\u00a0H. Gonnet (Ed.). ACM, 357\u2013363. https:\/\/doi.org\/10.1145\/74540.74582"},{"key":"e_1_3_2_1_21_1","volume-title":"Term Rewriting Systems","unstructured":"Terese. 2003. Term Rewriting Systems . In Cambridge Tracts in Theoretical Computer Science, M. Bezem, J. W. Klop & R. de Vrijer eds. Cambridge University Press . Terese. 2003. Term Rewriting Systems. In Cambridge Tracts in Theoretical Computer Science, M. Bezem, J. W. Klop & R. de Vrijer eds. Cambridge University Press."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)00023-K"}],"event":{"name":"PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming","location":"Tallinn Estonia","acronym":"PPDP 2021"},"container-title":["23rd International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479403","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3479394.3479403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479403"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,6]]},"references-count":22,"alternative-id":["10.1145\/3479394.3479403","10.1145\/3479394"],"URL":"https:\/\/doi.org\/10.1145\/3479394.3479403","relation":{},"subject":[],"published":{"date-parts":[[2021,9,6]]},"assertion":[{"value":"2021-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}