Category Theoretic Models of Data Refinement

M Johnson; D Naumann; J Power

doi:10.1016/j.entcs.2008.12.064

Category Theoretic Models of Data Refinement

M Johnson, D Naumann, J Power

Department of Computer Science

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

3 Citations (SciVal)

174 Downloads (Pure)

Abstract

We give an account of the use of category theory in modelling data refinement over the past twenty years. We start with Tony Hoare's formulation of data refinement in category theoretic terms, explain how the category theory may be made precise in generality and with elegance, using the notion of structure respecting lax transformation, for a first order imperative language, then study two main alternatives for extending that category theoretic analysis in order to account for higher order languages. The first is given by adjoint simulations; the second is given by the notion of lax logical relation. These provide techniques that can be used for a combined language, such as an imperative language with procedure passing.

Original language	English
Pages (from-to)	21-38
Number of pages	18
Journal	Electronic Notes in Theoretical Computer Science
Volume	225
DOIs	https://doi.org/10.1016/j.entcs.2008.12.064
Publication status	Published - 2 Jan 2009

Access to Document

10.1016/j.entcs.2008.12.064

Power_ENTCS_2009_225_21.pdf
NOTICE: this is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Electronic Notes in Theoretical Computer Science, vol 225, 2009, DOI 10.1016/j.entcs.2008.12.064
Accepted author manuscript, 1.05 MB

Cite this

@article{daeb5d2805634f54897a1046fbd8fb17,

title = "Category Theoretic Models of Data Refinement",

abstract = "We give an account of the use of category theory in modelling data refinement over the past twenty years. We start with Tony Hoare's formulation of data refinement in category theoretic terms, explain how the category theory may be made precise in generality and with elegance, using the notion of structure respecting lax transformation, for a first order imperative language, then study two main alternatives for extending that category theoretic analysis in order to account for higher order languages. The first is given by adjoint simulations; the second is given by the notion of lax logical relation. These provide techniques that can be used for a combined language, such as an imperative language with procedure passing.",

author = "M Johnson and D Naumann and J Power",

year = "2009",

month = jan,

day = "2",

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

language = "English",

volume = "225",

pages = "21--38",

journal = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Category Theoretic Models of Data Refinement

AU - Johnson, M

AU - Naumann, D

AU - Power, J

PY - 2009/1/2

Y1 - 2009/1/2

N2 - We give an account of the use of category theory in modelling data refinement over the past twenty years. We start with Tony Hoare's formulation of data refinement in category theoretic terms, explain how the category theory may be made precise in generality and with elegance, using the notion of structure respecting lax transformation, for a first order imperative language, then study two main alternatives for extending that category theoretic analysis in order to account for higher order languages. The first is given by adjoint simulations; the second is given by the notion of lax logical relation. These provide techniques that can be used for a combined language, such as an imperative language with procedure passing.

AB - We give an account of the use of category theory in modelling data refinement over the past twenty years. We start with Tony Hoare's formulation of data refinement in category theoretic terms, explain how the category theory may be made precise in generality and with elegance, using the notion of structure respecting lax transformation, for a first order imperative language, then study two main alternatives for extending that category theoretic analysis in order to account for higher order languages. The first is given by adjoint simulations; the second is given by the notion of lax logical relation. These provide techniques that can be used for a combined language, such as an imperative language with procedure passing.

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

UR - http://dx.doi.org/10.1016/j.entcs.2008.12.064

U2 - 10.1016/j.entcs.2008.12.064

DO - 10.1016/j.entcs.2008.12.064

M3 - Article

VL - 225

SP - 21

EP - 38

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Category Theoretic Models of Data Refinement

Abstract

Access to Document

Other files and links

Fingerprint

Cite this