Intel <-> (my prior Intel instruction semantics work on Conditional-Concurrent
C <-> Intel (using C0 from Pfenning at CMU?; GCL compiles to C)
Lisp <-> ACL2
Spad <-> COQ
Axiom uses Lisp integers for "NonNegativeIntegers". So there needs to be
proof systems like to use Peano posulates for "natural numbers" whereas
There are further questions which this does not address. For example, the
actual proof service to the Axiom compiler.
mentioned above, provide a server API which might be used to provide the
syntax/semantics. Axiom's compiler needs extensions. Systems like Lean,
This use of "existing empty Categories" (like Commutative) seems to be
for other signatures, using operations from the Domain.
creating a proof for each inherited signature, similar to the requirements
a Group has to "provide an implementation for the theorem signatures" by
proofs are essentially 'programs'. So, in Axiom-speak, a Domain which is
be a Group. The theorems themselves are essentially 'types' and the
Each of these theorems needs to be proven by a Domain which claims to
theorems that need to be proven by a Domain that is a Group.
existing Category structure. For example, Group could inherit a tower of
Similar towers of Theorem/Proof requirements can be built up using the
to provide an implementation (aka a proof) of commutativity.
Inheriting Commutative is no longer an empty promise. It requires a domain
commutative : TH -> PR
PR ==> Proof
TH ==> Theorem
Commutative : Category ==
such as "Commutative":
a well-defined type. The "type of a proof" is the statement of the theorem.
The essential idea (for Axiom) is that a proof is a first-class object with
a solid basis for implementing proofs in/of Axiom.
used at IBM. It seems that these systems are now capable of providing
and the systems are much more powerful than the Nthqm system I
The field of proof theory has grown beyond belief in the past decade
It seemed "interesting" but I didn't understand how important it is.
The Curry-Howard Isomorphism has been around since about 1969
I first heard of it in 2003 working with Gilbert Baumslag at CCNY.
In Axiom, that would be contained in the Category.
The "implementation of the type" is the proof itself. In Axiom. that would
be contained in the Domain, just like one would implement any other operation.
So, in Axiom terms, it is possible to give signatures in Axiom Categories,
For example (using Lean syntax http://leanprover.github.io/ ):
a reasonable place to insert theorem/proofs into Axiom's type tower.
At the moment, these are simply unproven declarations.
There are design questions of how to handle the 'forall', 'implies', and other
some path to provide "ground truth" to proofs, all the way down to the hardware.
The current path is a "tower of provers" extending from Spad to the hardware:
In the "upward" direction there needs to be some connection between the
theorems/proofs in a paper (e.g. integration, groebner, etc) and the Axiom
Spad implementations. I'm collecting references and decorating the algorithms
where I can find a connection. But that is only some groundwork. I have no
insight into this question yet. In the future there ought to be a stronger formal
connection between the published theory and its implementation in Axiom.
 Burns, Daly: "FXplorer: Exploration of Computed Software Behavior"
 Mili, Daly, Pleszkoch, Prowell HICSS 2006"A Sematic Recognizer Infrastructure for Computing Loop Behavior"
Axiom-developer mailing list
|Free forum by Nabble||Edit this page|