[Top][All Lists]

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

[Axiom-developer] MPL declarative style proofs

From: daly
Subject: [Axiom-developer] MPL declarative style proofs
Date: Sat, 18 Jul 2015 20:00:24 -0500

Very nice. 

I will try to use it as a first example. I've been concentrating
on the ACL2 level at the moment but I just changed Axiom to use
COQ on extracted proofs. Since this works from coqtop it looks like
I can use it for checking during the build.

Thanks for the reference.


reply via email to

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