((( [logo]Racket )))Need Help?
AboutDownloadDocumentationPLaneTCommunityLearning

[racket] Aging code -- Algol 68

From: Hendrik Boom (hendrik at topoi.pooq.com)
Date: Thu Jul 11 12:08:31 EDT 2013		 
On Thu, Jul 11, 2013 at 11:54:35AM -0400, Matthias Felleisen wrote:
> 
> What is a type=theoretical program verifier? How does it related to 
> modern things such as Coq/HOL/friends? 

It was an attempt to do something like coq and agda.

I managed to use it to verify a merge sort.  This was in the 80's.  I 
later heard about coq in the 90's or 00's.

-- hendrik
Posted on the users mailing list.