[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.
| 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

reply via email to

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