We give a category theoretic framework for data-refinement in call-by-value programming languages. One approach to data refinement for the simply typed #lambda#-calculus is given by generalising the notion of logical relation to one of lax logical relation, so that binary lax logical relations compose. So here, we generalise the notion of lax logical relation, defined in category theoretic terms, from the simply typed #lambda#-calculus to the computational #lambda#-calculus as a model of data refinement.
展开▼
