Pattern Unification for the Lambda Calculus with Linear and Affine Types

2010/09/14 by Anders Schack-Nielsen, Carsten Schürmann
Computer Science · #cs.LO

paper · pdf · doi:10.4204/eptcs.34.9

published as EPTCS 34, 2010, pp. 101-116 · In Proceedings LFMTP 2010, arXiv:1009.2189

arxiv created 2010/09/14 · arxiv updated 2010/09/16

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.

Citations

• Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice