Typed Unification for Deterministic Regular Types

This paper presents a new unification algorithm for terms interpreted in semantic domains denoted by a subclass of regular types called deterministic regular types. The algorithm handles the semantic universe as a partitioned collection of values, similar to data types in programming languages, and returns a most general unifier, failure, or a "wrong" result when terms belong to disjoint domains.