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

DOI10.1007/BF00885767MaRDI QIDQ1340967zbMATH OpenFDO

Authors Zhenyu Qian, Tobias Nipkow

Publication date 21 December 1994

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

Full work available at URL https://doi.org/10.1007/BF00885767

zbMATH Keywords

generic algorithm for preunification modulo \(\beta\eta\)- conversionhigher-order unificationreductionsimply typed \(\lambda\)-calculisubtypes

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1302672
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• Higher-order unification with dependent function types
• Subtyping + extensionality: confluence of \(\beta \eta\)top reduction in \(\mathrm{F}_\leq\)
• scientific article; zbMATH DE number 1332643

Cites work

• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• A semantics of multiple inheritance
• A unification algorithm for typed -calculus
• 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
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 1324447 (Why is no real title available?)
• scientific article; zbMATH DE number 1348466 (Why is no real title available?)
• scientific article; zbMATH DE number 512788 (Why is no real title available?)
• Proving and applying program transformations expressed with second-order patterns
• The lambda calculus. Its syntax and semantics. Rev. ed.
• TPS: A theorem-proving system for classical type theory
• Type inference with simple subtypes

Cited in

(5)

• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• scientific article; zbMATH DE number 1302672 (Why is no real title available?)
• scientific article; zbMATH DE number 1303341 (Why is no real title available?)
• scientific article; zbMATH DE number 1086659 (Why is no real title available?)
• scientific article; zbMATH DE number 1420794 (Why is no real title available?)

Describes a project that uses

Uses Software

• TPS

This page was built for publication: Reduction and unification in lambda calculi with a general notion of subtype

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1340967)