Bishop's work on Type Theory

[Martín Hötzel Escardó]

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