| ||||
| ||||
![]() Title:Nominal Techniques for Software Specification and Verification Authors:Maribel Fernandez Conference:CADE-29 Tags:alpha-equivalence, binder, nominal rewriting and nominal unification Abstract: The nominal approach to the specification of languages with binding operators, introduced by Gabbay and Pitts, has its roots in nominal set theory. With a user-friendly first-order syntax, nominal logic provides a formal framework to reason about binding operators similar to conventional, on-paper reasoning. Indeed, nominal logic uses the well-understood concept of permutation groups acting on sets to provide a rigorous first-order treatment for the common informal practice of fresh and bound names. In this talk, I will present our current work towards incorporating nominal techniques into two widely-used rule-based first-order verification environments: the K specification framework and the Maude programming environment. Nominal Techniques for Software Specification and Verification ![]() Nominal Techniques for Software Specification and Verification | ||||
Copyright © 2002 – 2025 EasyChair |