Recursive types are useful in encoding recursive data structures. Iso-recursive types are a popular method for handling recursive types in type systems. In iso-recursive type systems, explicit unfold/fold constructors are introduced in the term language to transform between a recursive type and its unfolded form. However, iso-recursive types have limitations when it comes to encoding certain programming language features, such as the nested composition of binary methods in the CP language. This seminar will introduce a new type system that extends the unfold/fold constructors in iso-recursive types to support “full iso-recursive typing”. This enhanced type system introduces a “cast” operator that allows for the conversion of subcomponent recursive types within a type, making the term language more flexible and expressive.