Pattern Unification for the Lambda Calculus with Linear and Affine Types
oleh: Anders Schack-Nielsen, Carsten Schürmann
| Format: | Article |
|---|---|
| Diterbitkan: | Open Publishing Association 2010-09-01 |
Deskripsi
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.