Hassen Saïdi
Unification dans le systeme T de Goedel.
Master Thesis (In french),
University of Paris 7, September 1994.
Abstract
We present in this work an extension of the Huet's higher-order unification algorithm to a lambda-calculus with a recursion operator (Goedel's system T). The algorithme (with some restrictions) is implemented in the caml-light language.