Hassen Saïdi

Unification dans le systeme T de Goedel.

Master Thesis (In french),

University of Paris 7, September 1994.


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.

Click here to get the postscript file of the full paper.