Module systems provide an important tool for structuring large programs to express their conceptual structure. In this seminar, we will present a new notion of intersection types for encoding module types. An algorithmic subtyping relation with type equality is defined for this notion of intersection types, and it can express inheritance of modules. The transitivity of subtyping is proved. We will also talk about the design of expressions and type systems for this notion of intersection types.