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.
ps
BibTeX:
@inproceedings{BerghoferN-TPHOLs00,
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},
year=2000,publisher=Springer,series=LNCS,volume=1869,pages="38--52"}