[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.
http://www.cs.nott.ac.uk/~jjw/papers/Compiler_Pearl/Compiler_Pearl.pdf
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.
Tim
- [Axiom-developer] Correctness/Provability/Compiling,
root <=