[TYPES] type systems in terms of contexts and judgements

Vladimir Voevodsky vladimir at ias.edu
Wed Jul 23 23:29:50 EDT 2014


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.



More information about the Types-list mailing list