We have nowadays a multitude, even a plethora, of different proof checkers and theorem provers. For the multitude of calculi and formal systems that have been developed by the theoretical computer science community for reasoning rigorously on the various properties of programs and processes. But building any of such formal computer systems is a very daunting task. And in fact one has to, building it from scratch I mean, and so it is crucial if we want to use various formal systems. It is often the case also that when you want to prove some property of your system, one particular logical system is not enough and you have to switch and perhaps prove as lemma using a different logical system from the one you are actually going to use for the proof of the final specification. So you actually need more than one implementation of your logical system. So is it possible to factor out commonalties across implementations of various formal systems so that we can implement them once and for all? Again type-functional language do offer an answer. And the answer is as I had anticipated logical frameworks. That is you can view typed functional languages as metalanguages for specifying logics and all the details of the inferential machinery, such as syntax, variable and schemata managing, rules, proofs, tactics. Then we can implement once and for all a proof editor for our metalanguage and here we are done, we can on demand tailor such a general implementation to the implementation for a specific formal system.

---