Category theoretic models of data refinement | Macquarie University ResearchOnline

Home

Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.14/146694

8 Visitors

9 Hits

0 Downloads

Title: Category theoretic models of data refinement
Related: Electronic notes in theoretical computer science, Vol. 225, (2008), p.21-38
DOI: 10.1016/j.entcs.2008.12.064
Publisher: Elsevier
Date: 2008
FoR/RFCD Code(s): 080200 Computation Theory and Mathematics
Author/Creator: Johnson, Michael
Author/Creator: Naumann, David
Author/Creator: Power, John
Description: 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.
Description: 18 page(s)
Subject Keyword: 080200 Computation Theory and Mathematics
Subject Keyword: data refinement
Subject Keyword: lax natural transformation
Subject Keyword: adjoint simulation
Subject Keyword: lax logical relation
Resource Type: journal article
Organisation: Macquarie University. Dept. of Computing

Macquarie University ResearchOnline