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 ____________________ Racket Users list: http://lists.racket-lang.org/users
