[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Correctness/Provability/Compiling
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-developer] Correctness/Provability/Compiling |
Date: |
24 Jul 2006 01:53:00 +0200 |
root <address@hidden> writes:
| 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.
We need a clear formulation of the type system for that.
Adn we also need a clear grammar.
| 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.
Funny, you should mention that. In our design for "C++ concepts", we
have provision for that -- though it is not enforced in the typpe
system directtly, but can be used for auxiliary tools.
-- Gaby