Matching logic is a formalism for specifying and reasoning about structures using patterns and pattern matching. Growing in popularity, matching logic has been used to define many logical systems such as separation logic with recursive definitions and linear-temporal logic. Despite this, there is no way for a user to define his or her own matching logic theories using a theorem prover, with maximal assurance of the properties being proved. Hence, in this work, we formalized a version of matching logic using the Coq proof assistant. Specifically, we create a new version of matching logic that uses a locally nameless representation, where quantified variables are unnamed in order to aid verification. We formalize the syntax, semantics, and proof system of this representation of matching logic using the Coq proof assistant. Crucially, we also verify the soundness of the formalized proof system, thereby guaranteeing that any matching logic properties proved in our Coq formalization are indeed correct. We believe this work provides a previously unexplored avenue for defining and proving matching logic theories and properties.
翻译:匹配逻辑是一种形式主义, 用于说明和推理使用模式和模式匹配的结构。 流行程度不断增长, 匹配逻辑被用来定义许多逻辑系统, 如分解逻辑, 包括递归定义和线性时时逻辑。 尽管如此, 用户无法使用理论证明来定义自己的匹配逻辑理论, 并最大限度地保证属性得到验证。 因此, 在这项工作中, 我们正式确定了使用 Coq 校对助理的匹配逻辑版本 。 具体地说, 我们创造了一个新的匹配逻辑版本, 使用本地无名称的表达法, 使用量化变量来帮助校验 。 我们用 Coq 校对助理来正式确定匹配逻辑的语法、 语义和验证系统 。 我们还验证了正式验证系统的正确性, 从而保证在 Coq 正式化中证明的任何匹配逻辑属性确实正确 。 我们相信, 这项工作为定义和证明匹配逻辑理论和属性提供了一条前所未有的途径 。