[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] PVS

From: daly
Subject: [Axiom-developer] PVS
Date: Mon, 26 May 2014 22:30:12 -0500

Thanks. I had not heard of PVS but I will look into it.

I have used ACL2 in the distant past and will have to get up
to speed on it again. I've downloaded and built the latest version.

I know that ACL2 is not capable of handling a Spad compiler but one
has to start somewhere. The important point, in my mind, is the focus
on some sort of proof in the long term.  We really need to have a
higher standard for computational mathematics, and, as they say,
"If not us, who? If not now, when?".

Matt Kaufmann and J Moore have always been quite helpful in the
past. I suspect they would be interested in any work we do in
this area.

Tim Daly

reply via email to

[Prev in Thread] Current Thread [Next in Thread]