Re: [TYPES] type systems in terms of contexts and judgements
Prof Robert Harper <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] 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 [email protected] ----------------------------- On Jul 23, 2014, at 23:29, Vladimir Voevodsky <[email protected]> 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. > >