Linear Higher-Order Pre-Unification (Extended Abstract)

We develop an efficient representation and a pre-unification algorithm in the style of Huet for the This extended abstract has been submitted to the CADE-13 Workshop on Proof Search in Type-Theoretic Languages Brunswick, NJ, July 30th 1996. linear -calculus !\Gammaffi&? which includes intuitionistic functions (!), linear functions (\Gammaffi), additive pairing (&), and additive unit (?). Potential applications lie in proof search, logic programming, and logical frameworks based on linear type theories. We also show that, surprisingly, a similar pre-unification algorithm does not exist for certain sublanguages. 1 Introduction Linear logic [Gir87] refines more traditional logical formalism with direct means of expressing common situations, especially those revolving around a notion of mutable state. Attempts at mechanizing this additional expressive power led to the design of several logic programming languages based on various fragments of linear logic. The only new aspect in the ..