Reflecting recursive types

Stream: Program verification

[Jakob von Raumer]

I'm trying to reflect a class of recursive types in a language with a type system close to the one of C into Lean types, does anyone know if there's any projects doing a similar thing already? For examples, embedded mu calculus expressions as well as a implmentation to quote them into lean types?