Proof terms for simply typed higher order logic

Stefan Berghofer and Tobias Nipkow

This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and reconstruction of proof terms are described and have been implemented in the theorem prover Isabelle. Experimental results confirm the effectiveness of the compression scheme.



author={Stefan Berghofer and Tobias Nipkow},
title={Proof terms for simply typed higher order logic},
booktitle={Theorem Proving in Higher Order Logics},
editor={J. Harrison and M. Aagaard},