Name
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1016/j.entcs.2008.12.064 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
imperative language,lax natural transformation,category theoretic models,combined language,lax transformation,lax logical relation,category theoretic analysis,data refinement,category theoretic term,category theory,higher order language,order imperative language,adjoint simulation,higher order,natural transformation,first order | Allegory,Higher order languages,First order,Computer science,Pure mathematics,Imperative programming,Theoretical computer science,Category theory,Elegance,Calculus,Generality | Journal |
Volume | ISSN | Citations |
225, | Electronic Notes in Theoretical Computer Science | 3 |
PageRank | References | Authors |
0.47 | 23 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael T. Johnson | 1 | 435 | 53.51 |
| David Naumann | 2 | 1101 | 84.12 |
| John Power | 3 | 77 | 7.79 |