[Agda] Bishop's work on Type Theory

[Martin Escardo]

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