Summary or recommendation responses (higher order logic)


Sorry for the delay in summarizing and reposting.  Here are the
recommendations I received for consistency proofs and for unification
algorithms in higher order logics.  Thanks once again to all the

Denby Wong


()  A typed operational semantics for type theory - Healfdene Goguen

()  Categorical logic and type theory - Bart Jacobs

()  Computation and reasoning: a type theory for computer science -
    Zhaohui Luo

()  Constructions, inductive types, and strong normalization -
    Thorsten Altenkirch

()  Semantics of type theory - Thomas Streicher

()  Une theorie des constructions inductive - Benjamin Werner


()  Gerard Huet.

()  Longo and Moggi