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.

Bibliographic Details
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
_version_ 1819032803265740800
author Anders Schack-Nielsen
Carsten Schürmann
author_facet Anders Schack-Nielsen
Carsten Schürmann
author_sort Anders Schack-Nielsen
collection DOAJ
description 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.
first_indexed 2024-12-21T07:07:45Z
format Article
id doaj.art-43446e5f6de04a96bed181eae1380d3c
institution Directory Open Access Journal
issn 2075-2180
language English
last_indexed 2024-12-21T07:07:45Z
publishDate 2010-09-01
publisher Open Publishing Association
record_format Article
series Electronic Proceedings in Theoretical Computer Science
spelling doaj.art-43446e5f6de04a96bed181eae1380d3c2022-12-21T19:12:04ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-09-0134Proc. LFMTP 201010111610.4204/EPTCS.34.9Pattern Unification for the Lambda Calculus with Linear and Affine TypesAnders Schack-NielsenCarsten SchürmannWe 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.http://arxiv.org/pdf/1009.2795v1
spellingShingle Anders Schack-Nielsen
Carsten Schürmann
Pattern Unification for the Lambda Calculus with Linear and Affine Types
Electronic Proceedings in Theoretical Computer Science
title Pattern Unification for the Lambda Calculus with Linear and Affine Types
title_full Pattern Unification for the Lambda Calculus with Linear and Affine Types
title_fullStr Pattern Unification for the Lambda Calculus with Linear and Affine Types
title_full_unstemmed Pattern Unification for the Lambda Calculus with Linear and Affine Types
title_short Pattern Unification for the Lambda Calculus with Linear and Affine Types
title_sort pattern unification for the lambda calculus with linear and affine types
url http://arxiv.org/pdf/1009.2795v1
work_keys_str_mv AT andersschacknielsen patternunificationforthelambdacalculuswithlinearandaffinetypes
AT carstenschurmann patternunificationforthelambdacalculuswithlinearandaffinetypes