[TYPES] type systems in terms of contexts and judgements

[Prof Robert Harper]

I don't know what would be the first occurrence, but the term "judgement" and the use of hypothetical judgments (for which he refers to de Bruijn's AUTOMATH) appears in Martin-Loef's "Constructive Mathematics and Computer Programming" from 1978.  He addressed the concepts head-on in his two papers on philosophical logic, called "On the meaning of the logical constants and the justifications of the logical laws" and "Truth of a proposition, evidence for a judgment".

-----------------------------
Prof Robert Harper
Carnegie Mellon CSD
rwh at cs.cmu.edu
-----------------------------



On Jul 23, 2014, at 23:29, Vladimir Voevodsky <vladimir at ias.edu> wrote:

> [ 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.
> 
>