{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T16:43:24Z","timestamp":1762447404779,"version":"build-2065373602"},"reference-count":29,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2023,9,21]],"date-time":"2023-09-21T00:00:00Z","timestamp":1695254400000},"content-version":"am","delay-in-days":263,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS 16-19275"],"award-info":[{"award-number":["CNS 16-19275"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-18-C-0092"],"award-info":[{"award-number":["FA8750-18-C-0092"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006831","name":"U.S. Air Force","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006831","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Logical and Algebraic Methods in Programming"],"published-print":{"date-parts":[[2023,1]]},"DOI":"10.1016\/j.jlamp.2022.100810","type":"journal-article","created":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T12:58:35Z","timestamp":1662469115000},"page":"100810","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Capturing constrained constructor patterns in matching logic"],"prefix":"10.1016","volume":"130","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3208-4061","authenticated-orcid":false,"given":"Xiaohong","family":"Chen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8097-040X","authenticated-orcid":false,"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jlamp.2022.100810_br0010","series-title":"Proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017)","first-page":"201","article-title":"A constructor-based reachability logic for rewrite theories","volume":"vol. 10855","author":"Skeirik","year":"2018"},{"issue":"4","key":"10.1016\/j.jlamp.2022.100810_br0020","doi-asserted-by":"crossref","first-page":"315","DOI":"10.3233\/FI-2020-1926","article-title":"A constructor-based reachability logic for rewrite theories","volume":"173","author":"Skeirik","year":"2020","journal-title":"Fundam. Inform."},{"issue":"7","key":"10.1016\/j.jlamp.2022.100810_br0030","doi-asserted-by":"crossref","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","article-title":"Twenty years of rewriting logic","volume":"81","author":"Meseguer","year":"2012","journal-title":"J. Log. Algebraic Program."},{"key":"10.1016\/j.jlamp.2022.100810_br0040","series-title":"Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM 2010)","first-page":"1","article-title":"Fostering proof scores in CafeOBJ","volume":"vol. 6447","author":"Futatsugi","year":"2010"},{"issue":"7\u20138","key":"10.1016\/j.jlamp.2022.100810_br0050","doi-asserted-by":"crossref","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","article-title":"Folding variant narrowing and optimal variant termination","volume":"81","author":"Escobar","year":"2012","journal-title":"J. Log. Algebraic Program."},{"key":"10.1016\/j.jlamp.2022.100810_br0060","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2017.09.001","article-title":"Variant-based satisfiability in initial algebras","volume":"154","author":"Meseguer","year":"2018","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"10.1016\/j.jlamp.2022.100810_br0070","first-page":"1","article-title":"Matching logic","volume":"13","author":"Ro\u015fu","year":"2017","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.jlamp.2022.100810_br0080","series-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2019)","first-page":"1","article-title":"Matching \u03bc-logic","author":"Chen","year":"2019"},{"author":"Chen","key":"10.1016\/j.jlamp.2022.100810_br0090"},{"key":"10.1016\/j.jlamp.2022.100810_br0100","series-title":"Proceedings of the 33rd International Conference on Computer-Aided Verification","first-page":"1","article-title":"Towards a trustworthy semantics-based language framework via proof generation","author":"Chen","year":"2021"},{"key":"10.1016\/j.jlamp.2022.100810_br0110","series-title":"Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Virtual Event, October 20-22, 2020, Revised Selected Papers","first-page":"19","article-title":"Connecting constrained constructor patterns and matching logic","volume":"vol. 12328","author":"Chen","year":"2020"},{"author":"Chen","key":"10.1016\/j.jlamp.2022.100810_br0120"},{"key":"10.1016\/j.jlamp.2022.100810_br0130","series-title":"Proceedings of the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO'19)","first-page":"1","article-title":"Matching mu-logic: foundation of k framework","volume":"vol. 139","author":"Chen","year":"2019"},{"key":"10.1016\/j.jlamp.2022.100810_br0140","series-title":"Engineering Trustworthy Software Systems","article-title":"SETSS'19 lecture notes on K","author":"Chen","year":"2019"},{"key":"10.1016\/j.jlamp.2022.100810_br0150","article-title":"A generic framework for symbolic execution: a coinductive approach","author":"Lucanu","year":"2016","journal-title":"J. Symb. Comput."},{"issue":"3","key":"10.1016\/j.jlamp.2022.100810_br0160","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.entcs.2009.05.015","article-title":"Variant narrowing and equational unification","volume":"238","author":"Escobar","year":"2009","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2022.100810_br0170","series-title":"Formal Methods\u2014The Next 30 Years","first-page":"502","article-title":"Unification in matching logic","volume":"vol. 11800","author":"Arusoaie","year":"2019"},{"issue":"2","key":"10.1016\/j.jlamp.2022.100810_br0180","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","article-title":"Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations","volume":"105","author":"Goguen","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2022.100810_br0190","series-title":"Recent Trends in Algebraic Development Techniques","first-page":"18","article-title":"Membership algebra as a logical framework for equational specification","volume":"vol. 1376","author":"Meseguer","year":"1997"},{"key":"10.1016\/j.jlamp.2022.100810_br0200","article-title":"Generalized rewrite theories, coherence completion, and symbolic methods","volume":"110","author":"Meseguer","year":"2020","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"ICFP","key":"10.1016\/j.jlamp.2022.100810_br0210","doi-asserted-by":"crossref","DOI":"10.1145\/3408970","article-title":"A general approach to define binders using matching logic","volume":"4","author":"Chen","year":"2020","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jlamp.2022.100810_br0220","article-title":"Matching logic explained","volume":"120","author":"Chen","year":"2021","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"2","key":"10.1016\/j.jlamp.2022.100810_br0230","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pac. J. Math."},{"issue":"3","key":"10.1016\/j.jlamp.2022.100810_br0240","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u03bc-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theor. Comput. Sci."},{"issue":"POPL","key":"10.1016\/j.jlamp.2022.100810_br0250","doi-asserted-by":"crossref","DOI":"10.1145\/3290315","article-title":"Constructing quotient inductive-inductive types","volume":"3","author":"Kaposi","year":"2019","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jlamp.2022.100810_br0260","series-title":"Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FOSSACS'20) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS'20)","first-page":"257","article-title":"Constructing infinitary quotient-inductive types","volume":"vol. 12077","author":"Fiore","year":"2020"},{"issue":"1","key":"10.1016\/j.jlamp.2022.100810_br0270","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditioned rewriting logic as a united model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2022.100810_br0280","series-title":"RTA-TLCA","first-page":"425","article-title":"All-path reachability logic","volume":"vol. 8560","author":"\u015etef\u0103nescu","year":"2014"},{"key":"10.1016\/j.jlamp.2022.100810_br0290","series-title":"LICS 2013","first-page":"358","article-title":"One-path reachability logic","author":"Ro\u015fu","year":"2013"}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220822000633?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220822000633?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T16:39:15Z","timestamp":1762447155000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220822000633"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1]]},"references-count":29,"alternative-id":["S2352220822000633"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2022.100810","relation":{},"ISSN":["2352-2208"],"issn-type":[{"type":"print","value":"2352-2208"}],"subject":[],"published":{"date-parts":[[2023,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Capturing constrained constructor patterns in matching logic","name":"articletitle","label":"Article Title"},{"value":"Journal of Logical and Algebraic Methods in Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jlamp.2022.100810","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2022 Elsevier Inc. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"100810"}}