Hello, I am looking for a reference to a paper or book where intuitionistic type theory (Martin-Lof type theory) was first formulated in terms of contexts and judgements. The foundational paper by Martin-Lof (1972) does not use contexts. Vladimir.