An operational domain-theoretic treatment of recursive types

摘要

We develop an operational domain theory for treating recursive types with respect torncontextual equivalence. The principal approach we take deviates from classical domainrntheory in that we do not produce the recursive types using the usual inverse limitsrnconstructions – we get them for free by working directly with the operational semantics. Byrnextending type expressions to functors between some ‘syntactic’ categories, we establishrnalgebraic compactness. To do this, we rely on an operational version of the minimalrninvariance property, for which we give a purely operational proof.