From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 4 May 2018 14:01:53 -0700 (PDT)
From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?=
 <escardo...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com>
Subject: Bishop's work on type theory
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_7717_1493746637.1525467713335"

------=_Part_7717_1493746637.1525467713335
Content-Type: multipart/alternative; 
	boundary="----=_Part_7718_1197445641.1525467713335"

------=_Part_7718_1197445641.1525467713335
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit

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


------=_Part_7718_1197445641.1525467713335
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: 7bit

<div dir="ltr"><div>This week I learned two interesting things that seem to be kept as a guarded secret:</div><div><br></div><div>(1) Errett Bishop reinvented type theory.</div><div>(2) He also explained how to compile it to Algol.</div><div><br></div><div>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, ...</div><div><br></div><div>&quot;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&quot;</div><div><br></div><div>This was in the late 1960&#39;s (or correct me). Here is a link to both manuscripts: http://www.cs.bham.ac.uk/~mhe/Bishop/</div><div><br></div><div>Greetings from Bonn.</div><div>Martin</div><div><br></div></div>
------=_Part_7718_1197445641.1525467713335--

------=_Part_7717_1493746637.1525467713335--