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: bibtex PDF

Comments and questions to:
For website issues: