Re: [HoTT] Bishop's work on type theory

[Bas Spitters <b.a.w.s...@gmail.com>]

Hi Martin,

These were discussed publically at some point. I've got them at around 2000.
We never put them on the web, because Bishop had decided not to publish them.
Since you are doing this now, it might be good to at least add a note
to that respect, so that people can put them in context.

See you in Bonn!

Bas

On Fri, May 4, 2018 at 11:01 PM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> This week I learned two interesting things that seem to be kept as a guarded
> secret:
>
> (1) Errett Bishop reinvented type theory.
> (2) He also explained how to compile it to Algol.
>
> I am adding a link to these two manuscripts. A nice quote from the second
> paper (Algol.pdf) is this, in my opinion, because it foresees things such as
> Agda, Coq, NuPrl, ...
>
> "The possibility of such a compilation demonstrates the existence of a new
> type of programming language, one that contains theorems, proofs,
> quantifications, and implications, in addition to the more conventional
> facilities for specifying algorithms"
>
> This was in the late 1960's (or correct me). Here is a link to both
> manuscripts: http://www.cs.bham.ac.uk/~mhe/Bishop/
>
> Greetings from Bonn.
> Martin
>
> --
> 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.