Hierarchical Nominal Terms and Their Theory of Rewriting

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


Nominal rewriting introduced a novel method of specifying rewriting on syntax-with-binding. We extend this treatment of rewriting with hierarchy of variables representing increasingly 'meta-level' variables, e.g. in hierarchical nominal term rewriting the meta-level unknowns (representing unknown terms) in a rewrite rule can be 'folded into' the syntax itself (and rewritten). To the extent that rewriting is a mathematical meta-framework for logic and computation, and nominal rewriting is a framework with native support for binders, hierarchical nominal term rewriting is a meta-to-the-omega level framework for logic and computation with binders. © 2007 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)37-52
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Issue number5
Publication statusPublished - 2 Jun 2007


  • meta-theory of logic and programming
  • Nominal rewriting
  • nominal techniques


Dive into the research topics of 'Hierarchical Nominal Terms and Their Theory of Rewriting'. Together they form a unique fingerprint.

Cite this