Extensions and applications of higher-order unification
Conal M. Elliott · 1990
... unification problems. Then, in this framework, we develop a new unification algorithm for a-calculus with dependent function (II) types. This algorithm is especially useful as it provides for mechanization in the very expressive Logical Framework (LF). The development (object-languages). The rich structure of a typed-calculus,asopposedtotraditional,rst- generalideaistousea-calculusasameta-languageforrepresentingvariousotherlanguages thelattercase,thealgorithmisincomplete,thoughstillquiteusefulinpractice. Thelastpartofthedissertationprovidesexamplesoftheusefulnessofthealgorithms.The algorithmrstfordependentproduct()types,andsecondforimplicitpolymorphism.In involvessignicantcomplicationsnotarisingHuet'scorrespondingalgorithmforthesimply orderabstractsyntaxtrees,allowsustoexpressrules,e.g.,programtransformationand typed-calculus,primarilybecauseitmustdealwithill-typedterms.Wethenextendthis Wecanthenuseunicationinthemeta-languagetomechanizeapplicationoftheserules.