{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T16:20:21Z","timestamp":1776183621053,"version":"3.50.1"},"reference-count":31,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T00:00:00Z","timestamp":1775606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"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":[[2026,6]]},"DOI":"10.1016\/j.jlamp.2026.101128","type":"journal-article","created":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T23:21:35Z","timestamp":1775517695000},"page":"101128","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Unification and anti-unification in applicative matching logic"],"prefix":"10.1016","volume":"150","author":[{"given":"\u00c1d\u00e1m","family":"Kurucz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3183-0712","authenticated-orcid":false,"given":"P\u00e9ter","family":"Bereczky","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0261-0091","authenticated-orcid":false,"given":"D\u00e1niel","family":"Horp\u00e1csi","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/j.jlamp.2026.101128_bib0001","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.jlamp.2026.101128_bib0002","series-title":"Formal Methods \u2013 the Next 30 Years","first-page":"502","article-title":"Unification in matching logic","author":"Arusoaie","year":"2019"},{"key":"10.1016\/j.jlamp.2026.101128_bib0003","series-title":"[1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science","first-page":"74","article-title":"Unification and anti-unification in the calculus of constructions","author":"Pfenning","year":"1991"},{"key":"10.1016\/j.jlamp.2026.101128_bib0004","series-title":"26th International Conference on Rewriting Techniques and Applications (RTA 2015)","first-page":"57","article-title":"Nominal anti-unification","volume":"36","author":"Baumgartner","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101128_bib0005","series-title":"Computer Aided Verification","first-page":"477","article-title":"Towards a trustworthy semantics-based language framework via proof generation","author":"Chen","year":"2021"},{"issue":"6","key":"10.1016\/j.jlamp.2026.101128_bib0006","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1145\/2813885.2737979","article-title":"Defining the undefinedness of C","volume":"50","author":"Hathhorn","year":"2015","journal-title":"ACM SIGPLAN Not."},{"key":"10.1016\/j.jlamp.2026.101128_bib0007","series-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"445","article-title":"K-Java: a complete semantics of Java","author":"Bogdanas","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101128_bib0008","series-title":"A Formal Semantics of Python 3.3","author":"Guth","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101128_bib0009","series-title":"2018 International Symposium on Theoretical Aspects of Software Engineering (TASE)","first-page":"44","article-title":"KRust: a formal executable semantics of Rust","author":"Wang","year":"2018"},{"key":"10.1016\/j.jlamp.2026.101128_bib0010","series-title":"Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","first-page":"1133","article-title":"A complete formal semantics of x86-64 user-level instruction set architecture","author":"Dasgupta","year":"2019"},{"key":"10.1016\/j.jlamp.2026.101128_bib0011","series-title":"2018 IEEE 31st Computer Security Foundations Symposium (CSF)","first-page":"204","article-title":"KEVM: a complete formal semantics of the Ethereum virtual machine","author":"Hildenbrandt","year":"2018"},{"key":"10.1016\/j.jlamp.2026.101128_bib0012","series-title":"Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","first-page":"1004","article-title":"Language-parametric compiler validation with application to LLVM","author":"Kasampalis","year":"2021"},{"key":"10.1016\/j.jlamp.2026.101128_bib0013","doi-asserted-by":"crossref","DOI":"10.23638\/LMCS-13(4:28)2017","article-title":"Matching logic","volume":"Volume 13, Issue 4","author":"Rosu","year":"2017","journal-title":"Logical Methods Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101128_bib0014","doi-asserted-by":"crossref","DOI":"10.4204\/EPTCS.369.1","article-title":"Proof-carrying parameters in certified symbolic execution: the case study of antiunification","volume":"369","author":"Arusoaie","year":"2022","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101128_bib0015","first-page":"153","article-title":"A note on inductive generalization","volume":"5","author":"Plotkin","year":"1970","journal-title":"Mach. Intell."},{"key":"10.1016\/j.jlamp.2026.101128_bib0016","series-title":"Technical Report","article-title":"Technical Report: Applicative Matching Logic: Semantics of K","author":"Chen","year":"2020"},{"key":"10.1016\/j.jlamp.2026.101128_bib0017","series-title":"Theoretical Aspects of Computing \u2013 ICTAC 2023","first-page":"139","article-title":"Interactive matching logic proofs in Coq","author":"Tu\u0161il","year":"2023"},{"key":"10.1016\/j.jlamp.2026.101128_bib0018","doi-asserted-by":"crossref","DOI":"10.1016\/j.jlamp.2021.100638","article-title":"Matching logic explained","volume":"120","author":"Chen","year":"2021","journal-title":"J. Logical Algebraic Methods Program."},{"key":"10.1016\/j.jlamp.2026.101128_bib0019","series-title":"2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","first-page":"1","article-title":"Matching \u03bc-logic","author":"Chen","year":"2019"},{"key":"10.1016\/j.jlamp.2026.101128_bib0020","unstructured":"HARP Project, AML-formalization, 2024. Accessed on April 30th, 2025, https:\/\/github.com\/harp-project\/AML-Formalization\/releases\/tag\/v1.0.16."},{"key":"10.1016\/j.jlamp.2026.101128_bib0021","doi-asserted-by":"crossref","DOI":"10.4204\/EPTCS.369.2","article-title":"Mechanizing matching logic in Coq","author":"Bereczky","year":"2022","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101128_bib0022","series-title":"Handbook of Automated Reasoning","first-page":"445","article-title":"Chapter 8 - unification theory","author":"Baader","year":"2001"},{"issue":"3","key":"10.1016\/j.jlamp.2026.101128_bib0023","doi-asserted-by":"crossref","first-page":"534","DOI":"10.1093\/jigpal\/jzad008","article-title":"Proof-carrying parameters in certified symbolic execution","volume":"32","author":"Arusoaie","year":"2023","journal-title":"Logic J. IGPL"},{"key":"10.1016\/j.jlamp.2026.101128_bib0024","series-title":"Handbook of Automated Reasoning","first-page":"1009","article-title":"Chapter 16 - higher-order unification and matching","author":"Dowek","year":"2001"},{"issue":"3","key":"10.1016\/j.jlamp.2026.101128_bib0025","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0743-1066(93)90039-J","article-title":"HiLog: a foundation for higher-order logic programming","volume":"15","author":"Chen","year":"1993","journal-title":"J. Logic Program."},{"key":"10.1016\/j.jlamp.2026.101128_bib0026","unstructured":"HARP Project, Unification in applicative matching logic, 2024a. Accessed on April 30th, 2025, https:\/\/github.com\/harp-project\/AML-Formalization\/pull\/431."},{"key":"10.1016\/j.jlamp.2026.101128_bib0027","unstructured":"H. Project, Anti-unification in applicative matching logic, 2024b, Accessed on April 30th, 2025, https:\/\/github.com\/harp-project\/AML-Formalization\/tree\/antiunification."},{"issue":"3","key":"10.1016\/j.jlamp.2026.101128_bib0028","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","article-title":"The locally nameless representation","volume":"49","author":"Chargu\u00e9raud","year":"2012","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.jlamp.2026.101128_bib0029","unstructured":"Iris project, STDPP: operations on sets, 2025. Accessed on April 30th, 2025, https:\/\/plv.mpi-sws.org\/coqdoc\/stdpp\/stdpp.base.html."},{"key":"10.1016\/j.jlamp.2026.101128_bib0030","series-title":"Handbook of Automated Reasoning","first-page":"179","article-title":"Chapter 4 - the inverse method","author":"Degtyarev","year":"2001"},{"key":"10.1016\/j.jlamp.2026.101128_bib0031","series-title":"Handbook of Automated Reasoning","first-page":"273","article-title":"Chapter 5 - normal form transformations","author":"Baaz","year":"2001"}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000209?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000209?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T15:28:28Z","timestamp":1776180508000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220826000209"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":31,"alternative-id":["S2352220826000209"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101128","relation":{},"ISSN":["2352-2208"],"issn-type":[{"value":"2352-2208","type":"print"}],"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Unification and anti-unification in applicative 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.2026.101128","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"101128"}}