Nominal Equational Logic

Ranald A. Clouston; Andrew M. Pitts

doi:10.1016/j.entcs.2007.02.009

Nominal Equational Logic

Ranald A. Clouston^*, Andrew M. Pitts

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

40 Citations (Scopus)

Abstract

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 language	English
Pages (from-to)	223-257
Number of pages	35
Journal	Electronic Notes in Theoretical Computer Science
Volume	172
DOIs	https://doi.org/10.1016/j.entcs.2007.02.009
Publication status	Published - 1 Apr 2007
Externally published	Yes

Access to Document

10.1016/j.entcs.2007.02.009

Cite this

@article{d170ddc07d364aabb9d6992c69227c1b,

title = "Nominal Equational Logic",

abstract = "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.",

keywords = "Equational logic, nominal sets, permutation actions, universal algebra",

author = "Clouston, {Ranald A.} and Pitts, {Andrew M.}",

year = "2007",

month = apr,

day = "1",

doi = "10.1016/j.entcs.2007.02.009",

language = "English",

volume = "172",

pages = "223--257",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Nominal Equational Logic

AU - Clouston, Ranald A.

AU - Pitts, Andrew M.

PY - 2007/4/1

Y1 - 2007/4/1

N2 - 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.

AB - 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.

KW - Equational logic

KW - nominal sets

KW - permutation actions

KW - universal algebra

UR - http://www.scopus.com/inward/record.url?scp=33847636768&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.02.009

DO - 10.1016/j.entcs.2007.02.009

M3 - Article

SN - 1571-0661

VL - 172

SP - 223

EP - 257

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Nominal Equational Logic

Abstract

Access to Document

Other files and links

Fingerprint

Cite this