Reflection is a system's ability to represent and control its own metalevel. In this way, very powerful techniques to extend, adapt, and modify a system become available. Many researchers have recognized the great importance and usefulness of reflection in program ming languages [39, 38, 41, 40, 18, 14, 29], in theorem-proving [42, 5, 36, 15, 1, 28, 11, 13], in concurrent and distributed computation [27, 33, 35], and in many other areas such as compilation, programming environments, operating systems, fault-tolerance, and databases (see [37, 17] for recent snapshots of research in reflection).
In spite of being a very important topic, the semantic foundations of reflection are not yet well understood. For the case of reflection in logical languages we have recently proposed a general axiomatic notion of reflective logic [8]. Our axioms are based on the theory of general logics [30]; they are formulated in a logic-independent way that makes the reflective logic an explicit parameter and does not depend on the particular details of each logic.