Sciweavers

TPHOL
2000
IEEE
13 years 9 months ago
Proof Terms for Simply Typed Higher Order Logic
Abstract. This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Unification-based algorithms for the compression and re...
Stefan Berghofer, Tobias Nipkow