[TYPES] type systems in terms of contexts and judgements

Vladimir Voevodsky <[email protected]>
Newsgroups gmane.comp.science.types
Message-ID <[email protected]> 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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.
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.