A theory system is a collection of interdependent theories, some if which stand in a meta/object relationship, forming an arbitrary number of metalevels. The main thesis of this chapter is that theory systems constitute a suitable formalism for constructing advanced applications in reasoning and software engineering. The Alloy language for defining theory systems is introduced, its syntax is defined and a collection of inference rules is presented. A number of problems suitable for theory systems are discussed, with program examples given in Alloy. Some current implementation issues and future extensions are discussed.