Semantics of type theory. Correctness, completeness and independence results. - Birkhäuser Verlag, 1991. - ( Progress in Theoretical Computer Science ).