Pattern Unification for the Lambda Calculus with Linear and Affine Types
Logic in Computer Science
2010-09-16 v1
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.
Cite
@article{arxiv.1009.2795,
title = {Pattern Unification for the Lambda Calculus with Linear and Affine Types},
author = {Anders Schack-Nielsen and Carsten Schürmann},
journal= {arXiv preprint arXiv:1009.2795},
year = {2010}
}
Comments
In Proceedings LFMTP 2010, arXiv:1009.2189