TITLE

Portable Higher Order Logic Proofs

ABSTRACT

Interactive theorem proving is tackling ever larger formalization and
verification projects, and there is a critical need for theory
engineering techniques to support these efforts. One such technique is
effective package management, which has the potential to simplify the
development of logical theories by precisely checking dependencies and
promoting re-use. The OpenTheory project aims to transfer the benefits
of package management to logical theories.  This talk presents the
OpenTheory article format, which supports higher order logic theories
being exported from one theorem prover, compressed by a stand-alone
tool, and imported into a different theorem prover.