| A Functorial Approach to Refinement (2007) | |||||||||||||||
Abstract | |||||||||||||||
| We introduce -algebras and -algebras as semantic domains for data refinement of imperative programming languages. The functorial semantics of -calculus is given by using the adjunction between the category of -algebras and the category of small locally ordered categories. We define the notion of upward and downward simulation between the interpretations of atomic commands, and refinements between the interpretations of commands, by using lax or oplax transformations. We show that the adjunction extends to an enriched adjunction in the sense of lax, and which provide the fundamental machinery in the proof of soundness and completeness of the downward simulation with respect to the refinement. | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||