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

Jamie Andrews andrews at
Fri Dec 5 16:28:03 EST 2003

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

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.

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.


More information about the Types-list mailing list