@inproceedings{eab8840ee4454a5c9cb229afdfc2910d,
title = "Proof terms for simply typed higher order logic",
abstract = "This paper presents proof terms for simply typed, intuitio-nistic 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",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000 ; Conference date: 14-08-2000 Through 18-08-2000",
year = "2000",
doi = "10.1007/3-540-44659-1_3",
language = "English",
isbn = "9783540678632",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "38--52",
editor = "Mark Aagaard and John Harrison",
booktitle = "Theorem Proving in Higher Order Logics - 13th International Conference, TPHOLs 2000, Proceedings",
}