Meta-programming with Theory Systems - Barklund, Jonas; Boberg, Katrin; Dell'Acqua, Pierangelo; Veanes, Margus (1995)
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.
This paper appears as a chapter in Metalogics and Logic Programming, edited by K. Apt and F. Turini, and published by MIT Press in 1995.