Rewriting with Extensional Polymorphic Lambda-Calculus

Abstract We provide a confluent and strongly normalizing rewriting system, based on expansion rules, for the extensional second order typed lambda calculus with product and unit types: this system corresponds to the Intuitionistic Positive Calculus with implication, conjunction, quantification over proposition and the constant True. This result is an important step towards a new theory of reduction based on expansion rules, and gives a natural interpretation to the notion of second order η-long normal forms used in higher order resolution and unification, that are here just the normal forms of our reduction system.

Authors

• Roberto Di Cosmo
• Delia Kesner

Keywords

No keywords are indexed for this paper.