Pattern Unification for the Lambda Calculus with Linear and Affine Types
Anders Schack-Nielsen (IT University of Copenhagen), Carsten, Sch\"urmann (IT University of Copenhagen)
TL;DR
This paper introduces a pattern fragment for higher-order unification in linear and affine type theories and provides a deterministic algorithm for computing most general unifiers.
Contribution
It defines a new pattern fragment for unification in linear and affine types and presents a deterministic unification algorithm.
Findings
The unification algorithm is proven to be correct and complete.
It efficiently computes most general unifiers in the pattern fragment.
The approach advances unification techniques in linear and affine type systems.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies