TY - JOUR
T1 - Category Theoretic Models of Data Refinement
AU - Johnson, Michael
AU - Naumann, David
AU - Power, John
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.
KW - adjoint simulation
KW - data refinement
KW - lax logical relation
KW - lax natural transformation
UR - http://www.scopus.com/inward/record.url?scp=58149308097&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=58149308097&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2008.12.064
DO - 10.1016/j.entcs.2008.12.064
M3 - Article
AN - SCOPUS:58149308097
SN - 1571-0661
VL - 225
SP - 21
EP - 38
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - C
ER -