Author: Sebastian Skalberg
Title: Porting Proofs Between HOL Implementations
Abstract: 
Many of the current HOL implementations (HOL, Isabelle/HOL, HOL Light) have
formulations of HOL that are similar enought to facilitate a straightforward
port of proof objects from one system to another.  In the talk, I will focus on
the addition of proof objects to HOL98 and the subsequent automatic porting of
over 2000 theorems from that system to Isabelle/HOL.