Pattern Unification for the Lambda Calculus with Linear and Affine Types
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.
Main Authors: | Anders Schack-Nielsen, Carsten Schürmann |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2010-09-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1009.2795v1 |
Similar Items
-
On the Elementary Affine Lambda-Calculus with and Without Fixed Points
by: Lê Thành Dũng Nguyen
Published: (2019-08-01) -
Strong Typed Böhm Theorem and Functional Completeness on the Linear Lambda Calculus
by: Satoshi Matsuoka
Published: (2016-04-01) -
A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
by: Pablo Arrighi, et al.
Published: (2012-07-01) -
Intersection types in lambda calculus and logic
by: Gilezan Silvia
Published: (1993) -
Categorical Models for a Semantically Linear Lambda-calculus
by: Marco Gaboardi, et al.
Published: (2010-03-01)