Nominal Equational Logic

Ranald A. Clouston*, Andrew M. Pitts

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

40 Citations (Scopus)


This paper studies the notion of "freshness" that often occurs in the meta-theory of computer science languages involving various kinds of names. Nominal Equational Logic is an extension of ordinary equational logic with assertions about the freshness of names. It is shown to be both sound and complete for the support interpretation of freshness and equality provided by the Gabbay-Pitts nominal sets model of names, binding and α-conversion.

Original languageEnglish
Pages (from-to)223-257
Number of pages35
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 1 Apr 2007
Externally publishedYes


Dive into the research topics of 'Nominal Equational Logic'. Together they form a unique fingerprint.

Cite this