Reduction and unification in lambda calculi with a general notion of subtype
type: Item
instance of: scholarly article
title: Reduction and unification in lambda calculi with a general notion of subtype
zbMATH Open document ID: 0808.03008
DOI: 10.1007/BF00885767
author: Zhenyu Qian
author: Tobias Nipkow
published in: Journal of Automated Reasoning
publication date: 1994-12-21T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 704961
zbMATH Keywords: simply typed \(\lambda\)-calculi
zbMATH Keywords: subtypes
zbMATH Keywords: reduction
zbMATH Keywords: higher-order unification
zbMATH Keywords: generic algorithm for preunification modulo \(\beta\eta\)- conversion
describes a project that uses: TPS
MaRDI profile type: Publication
cites work: TPS: A theorem-proving system for classical type theory
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: A semantics of multiple inheritance
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Proving and applying program transformations expressed with second-order patterns
cites work: Q3918095
cites work: Q4255519
cites work: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
cites work: Type inference with simple subtypes
cites work: Q4281481
cites work: Q4264719
cites work: An algebraic semantics of higher-order types with subtypes
cites work: Computational aspects of an order-sorted logic with term declarations
cites work: Higher-order unification revisited: Complete sets of transformations
cites work: A mechanical solution of Schubert's steamroller by many-sorted resolution
description: scientific article; zbMATH DE number 704961