[Prev][Next][Index][Thread]
Mutually recursive types
I'm wondering if anyone can point me to some literature with the
static and dynamic semantics worked out for a polymorphic predicative
F_\omega variant of the type lambda calculus that includes the details
of *mutually recursive types*. I need such a calculus to describe the
core IR of a compiler.
In theory the compiler IRs for the FLINT or TIL compilers should
suffice. Unfortunately all the published formal semantics for the IRs
only describe a toy fragement of the full IR leaving out the details
of mutually recursive types. The IL used in the Harper-Stone account
of SML is almost what I want, but its treatment of polymorphism is not
what I want. I've cobbled together a calculus myself which, I think is
"right" but I hate having the feeling that I'm reinventing the wheel,
and doing a very bad job at it.