Higher order unification via explicit substitutions
type: Item
instance of: scholarly article
title: Higher order unification via explicit substitutions
zbMATH Open document ID: 1005.03016
author: Gilles Dowek
author: Thérèse Hardin
author: Claude Kirchner
published in: Information and Computation
publication date: 2003-01-14T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 1853096
zbMATH Keywords: higher-order unification
zbMATH Keywords: lambda calculus
describes a project that uses: Automath
describes a project that uses: ETPS
MaRDI profile type: Publication
OpenAlex ID: W2132119724
cites work: Explicit substitutions
cites work: Resolution in type theory
cites work: Q4726218
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q3342534
cites work: On finite representations of infinite sequences of terms
cites work: Q5287527
cites work: Confluence properties of weak and strong calculi of explicit substitutions
cites work: Q5748888
cites work: Simulation of Turing machines by a regular rewrite rule
cites work: Q5667469
cites work: Q4385532
cites work: Higher-order unification via combinators
cites work: A combinatory logic approach to higher-order E-unification
cites work: A Complete Proof Synthesis Method for the Cube of Type Systems
cites work: The undecidability of the second-order unification problem
cites work: Dynamically-typed computations for order-sorted equational presentations
cites work: The undecidability of unification in third order logic
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Q3883561
cites work: Q3703312
cites work: Q4297316
cites work: Q4364370
cites work: Meta-rule synthesis from crossed rewrite systems
cites work: Q4274979
cites work: An Efficient Unification Algorithm
cites work: Completeness results for basic narrowing
cites work: A logic programming language with lambda-abstraction, function variables, and simple unification
cites work: Unification under a mixed prefix
cites work: Q4364378
cites work: Q5678447
cites work: Higher-order unification revisited: Complete sets of transformations
cites work: Instantiation theory. On the foundations of automated deduction
cites work: Q4938612
DOI: 10.1006/INCO.1999.2837
description: scientific article; zbMATH DE number 1853096