@inbook {OR06 ,
	title = {Pointfree Factorization of Operation Refinement},
	booktitle = {FM - Formal Methods 2006 },
	series = {LNCS},
	volume = {4085},
	year = {2006},
	pages = {236{\textendash}251},
	publisher = {Springer-Verlag},
	organization = {Springer-Verlag},
	address = {Ontario, Canada},
	abstract = {<p>The standard operation refinement ordering is a kind of {\textquotedblleft}meet of op- posites{\textquotedblright}: non-determinism reduction suggests {\textquotedblleft}smaller{\textquotedblright} behaviour while increase of definition suggests {\textquotedblleft}larger{\textquotedblright} behaviour. Groves{\textquoteright} factorization of this ordering into two simpler relations, one per refinement concern, makes it more mathe- matically tractable but is far from fully exploited in the literature. We present a pointfree theory for this factorization which is more agile and calculational than the standard set-theoretic approach. In particular, we show that factorization leads to a simple proof of structural refinement for arbitrary parametric types and ex- ploit factor instantiation across different subclasses of (relational) operation. The prospect of generalizing the factorization to coalgebraic refinement is discussed.</p>
},
	doi = {10.1007/11813040_17},
	author = {Jos{\'e} Nuno Oliveira and C. Rodrigues}
}