[Top][All Lists]

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

[Axiom-developer] Proving Axiom Correct

From: daly
Subject: [Axiom-developer] Proving Axiom Correct
Date: Thu, 16 Jul 2015 01:03:06 -0500

COQ is being used as the proof engine for Spad-level code.

The latest change will automatically extract literate chunks
labelled 'coq' into a separate location for the COQ proof engine.
This can be controlled from the make command line by adding COQ=coq.

ACL2, with its lisp-based syntax and semantics, is the appropriate
engine for proving the interpreter and compiler. COQ, with its
ability to form dependent types, is the appropriate engine for
proving the algebra. Thus we're able to use the best tool for
each level of abstraction.


reply via email to

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