We will show now how such metamodels can be used in application, and we will discuss the case of the two models that I mentioned earlier, that is l-calculus, and p-calculus, and show how to provide encodings in logical frameworks and in final semantics. And especially for the case of logical frameworks, we will discuss briefly how to develop the meta-theory of this calculus in Coq, using the theory of contexts, which is an axiomatic approach to meta-reasoning. I hope that, in this introductory lecture, at least a few points have been made clear. Formal methods are indeed the unique way by which we can deal with the software rigorously. Unfortunately there are a number, a multitude of such systems. And if we want to be able to develop reasonably the meta-theories of such systems, we have to conceive yet another abstraction level, that we call the level of metamodels, where we can focus on some general properties of these systems. So we have to conceive this extra level of metamodels. Now it is surprising that this extra level of metamodels is not the level of so called logical framework theories like set theory of first order logic. This is some kind of intermediate level between the level of formal system and the level of mathematical foundation of theories. Somehow computer science has indicated that it is convenient and logically conceivable an intermediate level.

---