Today's lecture will be devoted to computational metamodels. As we described in the introductory summary lecture we described, we introduced three different computational models and today we are going to discuss two different computational metamodels.
The first is logical frameworks, and it is based on constructive higher order type theory. Logical frameworks, with its constructive higher order co-inductive type theory, because we want to deal also with complex and recursive datatypes is essentially higher order dependent type l-calculus.
This is essentially, the idea of using this higher order co-inductive type theory as a specification language for representing syntax, for this we need a higher order co-inductive dependent types and a specification language for representing operational semantics and the inferential machinery and proof-theory using the higher order inpredicative type of propositions.
This use of higher order type theories as specification languages for representing formal logical systems are actually our first example of metamodel, because they provide a setting for developing formally the meta-theory of formal logics and calculi. And, as we will see, using possibly suitable non-logical axioms.