Conservative extensions, interpretations between theories and all that!

Abstract

About twenty years ago, together with a group of collaborators, some conjectures were developed about the fundamental principles of a theory of specification. These principles included the use of interpretations between theories to underpin the concept of representation and parameterisation, conservative extensions to underpin the concept of modularity and extraiogieal equality to deal with multiple representations. It was quickly realised that there were fundamental metalogical properties which amounte dto 'laws' of specification. An example is provided by the role of Craig interpolation in the composability of implementations and parameter instantiation. Further work on institutio nsadded some fundamental ideas about generalising some of these concepts to logics other than many sorted first order Iogie and pointed out the eategorieal nature of many of the constructions. Recent work has highlighted the possibility of 'intemalising' some of the meta concepts involved and led to a re-examination of the fundamental principles. For example, extralogieal equality and general interpretations are not as fundamental as we thoughttwenty years ago. The purpose of the paper is to present a retrospective on this work and outline the basic principles of a general theory of specification as we now see it.