We present a realizability interpretation of co-inductive types based on partial equivalence relations (per's). We extract from the per's interpretation sound rules to type recursive definitions. These recursive definitions are needed to introduce ‘infinite’ and ‘total’ objects of co-inductive type such as an infinite stream, a digital transducer, or a non-terminating process. We show that the proposed type system subsumes those studied by Coquand and Gimenez while still enjoying the basic syntactic properties of subject reduction and strong normalization with respect to a confluent rewriting system first put forward by Gimenez.