What people are saying - Write a review
We haven't found any reviews in the usual places.
A-terms abstract view algorithm for higher-order applied assume base type bound variables Cambridge Computer Laboratory CB2 3QG England complete set complete unification algorithm completeness theorem Computation 8 1989 coregularity defined denoted downward complete equations extension to Huet's first-order logic free variables function types Higher-Order Logic Huet Huet's algorithm incomplete inference rules infinite set Intuitionistic Type Theory J.A. Goguen Jouannaud L.C. Paulson language Haskell Lemma many-sorted Meseguer ML-style polymorphism n-expanded form normal form order-sorted unification partial order presolved form preunifier principal types programming language regular signature result type Rewrite Systems Schmidt-SchauB Section sequel set of type set of unifiers signature is unitary simply typed A-calculus single imitation step Smolka Snyder and Gallier solution F subsort reflecting take an abstract theorem provers type checking type classes type substitution type system type variables typed terms types of terms unification process University of Cambridge view of types Waldmann 25