Conservative extensions, interpretations between theories and all that!

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 extralogical equality to deal with multiple representations. It was quickly realised that there were fundamental metalogical properties which amounted to ‘laws’ of specification. An example is provided by the role of Craig interpolation in the composability of implementations and parameter instantiation. Further work on institutions added some fundamental ideas about generalising some of these concepts to logics other than many sorted first order logic and pointed out the categorical nature of many of the constructions. Recent work has highlighted the possibility of ‘internalising’ some of the meta concepts involved and led to a re-examination of the fundamental principles. For example, extralogical equality and general interpretations are not as fundamental as we thought twenty 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.