Nominal Lawvere Theories: A category theoretic account of equational theories with names

Ranald Clouston

doi:10.1016/j.jcss.2014.04.002

Nominal Lawvere Theories: A category theoretic account of equational theories with names

Ranald Clouston^*

^*Corresponding author for this work

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

3 Citations (Scopus)

Abstract

Names, or object-level variables, are a ubiquitous feature in programming languages and other computational applications. Reasoning with names, and related constructs like binding and freshness, often poses conceptual and technical challenges. Nominal Equational Logic (NEL) is a logic for reasoning about equations in the presence of freshness side conditions. This paper gives a category theoretic account of NEL theories, by analogy with Lawvere's classic correspondence between equational theories and small categories with finite products. This development reveals the abstract structure behind reasoning with equations modulo freshness.

Original language	English
Pages (from-to)	1067-1086
Number of pages	20
Journal	Journal of Computer and System Sciences
Volume	80
Issue number	6
DOIs	https://doi.org/10.1016/j.jcss.2014.04.002
Publication status	Published - Sept 2014

Access to Document

10.1016/j.jcss.2014.04.002

Cite this

@article{c958af6f8296485688f7b86eb6b0fc01,

title = "Nominal Lawvere Theories: A category theoretic account of equational theories with names",

abstract = "Names, or object-level variables, are a ubiquitous feature in programming languages and other computational applications. Reasoning with names, and related constructs like binding and freshness, often poses conceptual and technical challenges. Nominal Equational Logic (NEL) is a logic for reasoning about equations in the presence of freshness side conditions. This paper gives a category theoretic account of NEL theories, by analogy with Lawvere's classic correspondence between equational theories and small categories with finite products. This development reveals the abstract structure behind reasoning with equations modulo freshness.",

keywords = "Equational logic, Fresh names, Lawvere Theories, Nominal sets, Permutation actions",

author = "Ranald Clouston",

year = "2014",

month = sep,

doi = "10.1016/j.jcss.2014.04.002",

language = "English",

volume = "80",

pages = "1067--1086",

journal = "Journal of Computer and System Sciences",

issn = "0022-0000",

publisher = "Academic Press Inc.",

number = "6",

}

TY - JOUR

T1 - Nominal Lawvere Theories

T2 - A category theoretic account of equational theories with names

AU - Clouston, Ranald

PY - 2014/9

Y1 - 2014/9

N2 - Names, or object-level variables, are a ubiquitous feature in programming languages and other computational applications. Reasoning with names, and related constructs like binding and freshness, often poses conceptual and technical challenges. Nominal Equational Logic (NEL) is a logic for reasoning about equations in the presence of freshness side conditions. This paper gives a category theoretic account of NEL theories, by analogy with Lawvere's classic correspondence between equational theories and small categories with finite products. This development reveals the abstract structure behind reasoning with equations modulo freshness.

AB - Names, or object-level variables, are a ubiquitous feature in programming languages and other computational applications. Reasoning with names, and related constructs like binding and freshness, often poses conceptual and technical challenges. Nominal Equational Logic (NEL) is a logic for reasoning about equations in the presence of freshness side conditions. This paper gives a category theoretic account of NEL theories, by analogy with Lawvere's classic correspondence between equational theories and small categories with finite products. This development reveals the abstract structure behind reasoning with equations modulo freshness.

KW - Equational logic

KW - Fresh names

KW - Lawvere Theories

KW - Nominal sets

KW - Permutation actions

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

U2 - 10.1016/j.jcss.2014.04.002

DO - 10.1016/j.jcss.2014.04.002

M3 - Article

SN - 0022-0000

VL - 80

SP - 1067

EP - 1086

JO - Journal of Computer and System Sciences

JF - Journal of Computer and System Sciences

IS - 6

ER -

Nominal Lawvere Theories: A category theoretic account of equational theories with names

Abstract

Access to Document

Other files and links

Fingerprint

Cite this