Pattern Unification for the Lambda Calculus with Linear and Affine Types

Anders Schack-Nielsen
(IT University of Copenhagen) 		Carsten Schürmann
(IT University of Copenhagen)

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 Karl Crary and Marino Miculan: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010), Edinburgh, UK, 14th July 2010, Electronic Proceedings in Theoretical Computer Science 34, pp. 101–116.
Published: 11th September 2010.
ArXived at: https://dx.doi.org/10.4204/EPTCS.34.9 bibtex PDF
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org