Request for literature recommendations.


Does anybody have any recommendations or pointers to the literature
for showing consistency in typed higher-order logics?  If so, could
you email them to me please.  Most helpful presently would be
intro/intermediate level material in either proof or model theoretic
approaches but any suggestions will be much appreciated.

Also, if someone knows where I might find material on unification
algorithms for typed higher order logics (other than those for the
simply typed case) please email these to me as well.

I will summarize and post all suggestions.

Denby Wong