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

DOI10.1007/BF00885767zbMATH Open0808.03008MaRDI QIDQ1340967FDOQ1340967

Authors: Zhenyu Qian, Tobias Nipkow 

Publication date: 21 December 1994

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

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

zbMATH Keywords

reductionsubtypeshigher-order unificationgeneric 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)

Cites Work

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

Cited In (4)

• Title not available (Why is that?)
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• Title not available (Why is that?)
• Title not available (Why is that?)

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)