Functorial semantics of first-order views

We provide a precise mathematical definition for first-order views used in parameterised specifications and we also provide a dual semantics for them that captures both their syntactic and model theoretic effects. We show that this semantics is functorial. Parameter instantiation is defined here as a (special kind of) pushout in the category of views; moreover the corresponding pushout squares are shown to enjoy a crucial model amalgamation property that ensures the consistency of the parameter instantiation process.