So, in order to highlight or to abstract away certain features, the kind
of metamodels that we described earlier seem to be convenient. Let me
give you an example or examples of these pervasive concepts. For instance,
as far when we discuss the case of logical frameworks, we have as a crucial
concept the inferential machinery or consisting of rule application and
hypothetical general inference. When we combine this pervasive concept
with the so called Higher Order Abstract Syntax, which is a generalisation
of the so-called algebraic context free grammars, well we hear we have
some kind of specifically computational concept, that of course could
be well described in set theory perhaps, or could be described in first
order logic, but when we describe it in constructive type theory it is
particularly natural. | ![]() |