Monads, predicates, and categorical logic programming
James Lipton, Robert W. McGrail · 1999
A framework for writing executable declarative specifications which incorporate categorical constraints on data, Horn Clauses, and monad and datatype specification over certain categories is defined. In particular, a generic extension of the base syntactic category in which arrows correspond to resolution proofs subject to the specified data constraints is constructed. Moreover, this dissertation yields a new canonical characterization of non-deterministic SLD resolution.