[Prev][Next][Index][Thread]
Summary or recommendation responses (higher order logic)
Hello,
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
respondents.
Denby Wong
=================================================================
Books/Dissertations:
() 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
General:
() Gerard Huet.
() Longo and Moggi