As a meta-language for formally expressing components and software developments an extension of ECC [Luo 91] is used. This is a very powerful calculus in which module concepts and polymorphism can be expressed adequately with the help of dependent products and dependent sums. A hierarchy of universes allows to describe programming and meta- programming as well as reasoning and meta-reasoning in the same framework.