[TYPES] subtyping of mutually recursive algebraic data types

[Aaron Gray]

I am interested if there is any work on the subtyping of mutually
recursive algebraic data types. I am wanting an algorithm for purposes
of implementing an object oriented programming language with ADT's
which lower onto a virtual class implementation which can support
mutually recursive behavior, but need the typ checking and inference
at the ADT level.

Theres a number of papers and projects in this area I have came across
but none of them actually tackle algebraic data types properly let
alone mutually recursive ones.

A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation.

- Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre
and Christophe Raffalli - subml - https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ 
- The Simple Essence of Algebraic Subtyping, Lionel Parreaux and
simple-sub implementation - https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ 
- A Mechanical Soundness Proof for Subtyping Over Recursive Types
Timothy Jones David J. Pearce -
https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ 

None of these seem to deal with mutually recursive data types.

I am interested in the papproach of using codata/coinduction and
coalgebras and possibly bisimulation in order to deal with the
mutually recursive nature of real world mutually recursive algebraic
data types like for instance AST's of real world complex computer
languages.

Any projects, papers, thoughts, or implementations would be of interest.

Regards,

Aaron