Tech report: "Cut Elimination for a Weakly Typed Higher Order Logic"

[Jamie Andrews]

Readers might be interested in the following technical report,
now available on

http://www.csd.uwo.ca/faculty/andrews/papers/

James H. Andrews. "Cut Elimination for a Weakly Typed Higher
Order Logic."  Technical Report No. 611, Department of Computer
Science, University of Western Ontario, December 2003.

Abstract:
Cut-elimination is proved for a weakly-typed higher order logic
based on those presented by Gilmore. The logic allows
lambda-abstraction over terms and formulas, permitting all terms
of the untyped lambda calculus including the Y combinator, and
providing various methods of expressing recursive functions and
predicates.  Consistency is achieved in the logic via a
nominalist distinction between use and mention of terms. This
report is intended as a companion to Andrews, "A Weakly-Typed
Logic with General Lambda Terms and Y-Combinator", Works in
Progress Track, TPHOLs 2002, which presented the syntax,
semantics and consistency of the logic.

cheers
--Jamie.