Skip navigation
Skip navigation

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

Clouston, Ranald

Description

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...[Show more]

dc.contributor.authorClouston, Ranald
dc.date.accessioned2015-12-10T23:23:11Z
dc.identifier.issn0022-0000
dc.identifier.urihttp://hdl.handle.net/1885/66843
dc.description.abstractNames, 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.
dc.publisherAcademic Press
dc.sourceJournal of Computer and System Sciences
dc.titleNominal Lawvere Theories: A category theoretic account of equational theories with names
dc.typeJournal article
local.description.notesImported from ARIES
local.identifier.citationvolume80
dc.date.issued2014
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.absfor010103 - Category Theory, K Theory, Homological Algebra
local.identifier.ariespublicationu4334215xPUB1354
local.type.statusPublished Version
local.contributor.affiliationClouston, Ranald, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.issue6
local.bibliographicCitation.startpage1067
local.bibliographicCitation.lastpage1086
local.identifier.doi10.1016/j.jcss.2014.04.002
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
dc.date.updated2015-12-10T10:37:26Z
local.identifier.scopusID2-s2.0-84901193966
local.identifier.thomsonID000336561300004
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Clouston_Nominal_Lawvere_Theories:_A_2014.pdf411.42 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator