  Matching logic is a formalism for specifying, and reasoning about,
mathematical structures, using patterns and pattern matching. Growing in
popularity, it has been used to define many logical systems such as separation
logic with recursive definitions and linear temporal logic. In addition, it
serves as the logical foundation of the K semantic framework, which was used to
build practical verifiers for a number of real-world languages. Despite being a
fundamental formal system accommodating substantial theories, matching logic
lacks a general-purpose, machine-checked formalization. Hence, we formalize
matching logic using the Coq proof assistant. Specifically, we create a new
representation of matching logic that uses a locally nameless encoding, and we
formalize the syntax, semantics, and proof system of this representation in the
Coq proof assistant. Crucially, we prove the soundness of the formalized proof
system and provide a means to carry out interactive matching logic reasoning in
Coq. We believe this work provides a previously unexplored avenue for reasoning
about matching logic, its models, and the proof system.
