Martin-Löf '86

Martin-Löf '86

[Colin Zwanziger]

[-- Attachment #1: Type: text/plain, Size: 269 bytes --]

Dear all,

Does anyone happen to have a copy of the work

Martin-Löf, P. (1986). Amendment to intuitionistic type theory. *Notes from
a lecture given in Göteborg*.

that they could share? Or advice on how to obtain a copy?

Best regards,

Colin Zwanziger

[-- Attachment #2: Type: text/html, Size: 362 bytes --]

Re: [HoTT] Martin-Löf '86

[Andrej Bauer]

[-- Attachment #1: Type: text/plain, Size: 153 bytes --]

Alas, it's not listed at https://github.com/michaelt/martin-lof (which is
otherwise a useful resource to be aware of).

With kind regards,

Andrej

[-- Attachment #2: Type: text/html, Size: 290 bytes --]

Re: [HoTT] Martin-Löf '86

[Ansten Mørch Klev]

[-- Attachment #1: Type: text/plain, Size: 1262 bytes --]

In light of the title and date of this lecture it is natural to think that
it presented the hierarchy of higher types, what is also sometimes called
the logical framework of Martin-Löf type theory. A good published reference
for this is the chapter by Nordström, Petersson, and Smith in vol 5 of the
Handbook of Logic in Computer Science. For the treatment of Pi, which here
allows for an induction principle, see also chapter 7 of the book by the
same authors and Garner's paper "On the strength of dependent products in
the type theory of Martin-Löf".

Ansten Klev

On Thu, Apr 26, 2018 at 8:56 PM, Colin Zwanziger <zwanz...@gmail.com>
wrote:

> Dear all,
>
> Does anyone happen to have a copy of the work
>
> Martin-Löf, P. (1986). Amendment to intuitionistic type theory. *Notes
> from a lecture given in Göteborg*.
>
> that they could share? Or advice on how to obtain a copy?
>
> Best regards,
>
> Colin Zwanziger
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 2006 bytes --]

Re: [HoTT] Martin-Löf '86

[Colin Zwanziger]

[-- Attachment #1: Type: text/plain, Size: 1722 bytes --]

Yes, this was when Martin-Löf introduced his logical framework formulation
of type theory. In addition, he returned to intensional type theory in that
lecture after some time working with extensional type theory. (I was able
to get a good sense of the content of the lecture via off-list responses.)

Best,

Colin

On Fri, May 4, 2018 at 10:47 AM, Ansten Mørch Klev <anste...@gmail.com>
wrote:

> In light of the title and date of this lecture it is natural to think that
> it presented the hierarchy of higher types, what is also sometimes called
> the logical framework of Martin-Löf type theory. A good published reference
> for this is the chapter by Nordström, Petersson, and Smith in vol 5 of the
> Handbook of Logic in Computer Science. For the treatment of Pi, which here
> allows for an induction principle, see also chapter 7 of the book by the
> same authors and Garner's paper "On the strength of dependent products in
> the type theory of Martin-Löf".
>
> Ansten Klev
>
> On Thu, Apr 26, 2018 at 8:56 PM, Colin Zwanziger <zwanz...@gmail.com>
> wrote:
>
>> Dear all,
>>
>> Does anyone happen to have a copy of the work
>>
>> Martin-Löf, P. (1986). Amendment to intuitionistic type theory. *Notes
>> from a lecture given in Göteborg*.
>>
>> that they could share? Or advice on how to obtain a copy?
>>
>> Best regards,
>>
>> Colin Zwanziger
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
>

[-- Attachment #2: Type: text/html, Size: 2980 bytes --]