REPRESENTING HIGHER-ORDER LOGIC PROOFS IN HOL

We describe an embedding of higher order logic in the HOL theorem prov ing system. Types, terms, sequents and inferences are represented as n ew types in the logic of the HOL system, and notions of proof and prov ability are defined. Using this formalisation, it is possible to reaso n about the correctness of derived rules of inference and about the re lations between different notions of proofs. The formalisation is also intended to make it possible to reason about programs that handle pro ofs as their data (e.g., proof checkers).