Martin Escardo
2018-05-04 23:08:27 UTC
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
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