Tech report: "Cut Elimination for a Weakly Typed Higher Order Logic"
andrews at csd.uwo.ca
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