[Top][All Lists]

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

[Axiom-developer] Correctness/Provability/Compiling

From: root
Subject: [Axiom-developer] Correctness/Provability/Compiling
Date: Sun, 23 Jul 2006 18:47:34 -0400

Functional Pearl, A Type-correct, stack-safe, provably correct
expression compiler in Epigram.

I've mentioned before that it is a long term goal of Axiom to 
enhance the compiler to prove properties of Categores and Domains.
This is of interest because of that goal. I'd like to be able to
do things like decorate the Categories and Domains with mathematical
axioms (e.g. Group) and prove properties like commutative rather
than just assert them. 


reply via email to

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