Nominal unification
type: Item
instance of: scholarly article
title: Nominal unification
zbMATH Open document ID: 1078.68140
author: Christian Urban
author: Andrew M. Pitts
author: Murdoch J. Gabbay
published in: Theoretical Computer Science
publication date: 2004-10-01T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 2105265
zbMATH Keywords: Abstract syntax
zbMATH Keywords: Alpha-conversion
zbMATH Keywords: Binding operations
zbMATH Keywords: Unification
describes a project that uses: ML
describes a project that uses: SLMC
describes a project that uses: Freshml
describes a project that uses: Qu-Prolog
MaRDI profile type: Publication
full work available at URL: j.tcs.2004.06.016
OpenAlex ID: W2912255765
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q4484489
cites work: Q4417861
cites work: Higher-order unification and matching
cites work: Higher order unification via explicit substitutions
cites work: A new approach to abstract syntax with variable binding
cites work: Q4288818
cites work: Q5714443
cites work: A typed context calculus
cites work: Q4535076
cites work: Q4023900
cites work: An Efficient Unification Algorithm
cites work: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
cites work: A calculus of mobile processes. II
cites work: The Qu-Prolog unification algorithm: formalisation and correctness
cites work: Linear unification
cites work: Nominal logic, a first order theory of names and binding
cites work: Q4495854
cites work: Unification of higher-order patterns in linear time and space
cites work: On the algebraic models of lambda calculus
cites work: Q4413069
cites work: Computer Science Logic
cites work: FreshML
DOI: 10.1016/J.TCS.2004.06.016
description: scientific article; zbMATH DE number 2105265