Reduction and unification in lambda calculi with a general notion of subtype

DOI10.1007/BF00885767zbMath0808.03008MaRDI QIDQ1340967

Tobias Nipkow, Zhenyu Qian

Publication date: 21 December 1994

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

reductionhigher-order unificationsubtypesgeneric algorithm for preunification modulo \(\beta\eta\)- conversionsimply typed \(\lambda\)-calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Uses Software

• TPS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• A semantics of multiple inheritance
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Proving and applying program transformations expressed with second-order patterns
• An algebraic semantics of higher-order types with subtypes
• Computational aspects of an order-sorted logic with term declarations
• Higher-order unification revisited: Complete sets of transformations
• TPS: A theorem-proving system for classical type theory
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Type inference with simple subtypes