• Do modules need to be type-checked in the kernel?
• Applicative vs generative functors
• Module and functor transparency
• Subtyping inductive types as definitions
• How far can modules and module types be identified?
• Towards a richer algebraic language of module constructions