Pattern Unification for the Lambda Calculus with Linear and Affine Types
arXiv:1009.2795 · doi:10.4204/EPTCS.34.9
Abstract
We define the pattern fragment for higher-order unification problems in linear and affine type theory and give a deterministic unification algorithm that computes most general unifiers.
In Proceedings LFMTP 2010, arXiv:1009.2189