In this paper we address the issue of scalability in formal systems that use higher order logic. We present a modular logical framework in which logical theories are constructed as logical modules. Like other logical frameworks such as Isabelle and LF, the framework allows the definition of general higher order logics. We introduce three new features to address the scalability problem: relating results formalized in different theories; allowing the definition of new computation systems; and integrating the logical theories with the implementation language.
We have implemented the framework, which we call MetaPRL. MetaPRL addresses system scalability by introducing separate compilation and verification of theory modules, and it supports interoperability of formal systems by providing abstract logical characterizations of systems.
Logics are constructed using an inheritance hierarchy. MetaPRL retains the tactic-tree proofs of , but the tactics (and other heuristics) are modularized to conform to the inheritance hierarchy. We have implemented several theories in MetaPRL, including the type theory, and a theory of Objective Caml. Our future plans include a connection between the logics of and HOL, based on Howe's semantics, with the eventual goal of interoperation between the two systems.
The paper is unpublished while I add a section on the theory foundation. Here is a preliminary version Postscript, PDF.