A semantic basis for logic-independent transformation

This paper is based on previous work by Harper, Sannella and Tarlecki who suggest a framework for giving semantic interpretations to logic representations in the LF logical framework. Besides LF, there are also other approaches that tackle the representation of logics in a meta-logic. The logic-independent aspect in the formal development of software has been investigated intensively based on abstract model theory. Less attention is paid to the proof system aspect. In this paper we treat logic-independence by considering the consequence relation that models a proof system for a logic. The existing work is generalized here to the consideration of any logic as a meta-logic, since there may be meta-logics other than LF that are more suitable and convenient for developing “object” logical systems. This generalized framework is then used for building logic-independent specifications and developments. The setting can eventually be considered as a firm semantic basis for developing logic-independent transformations.