[Aldor-l] [Axiom-developer] spad: language and compiler

[Jacques Carette]

Gabriel Dos Reis wrote:
> With Type:Type, it is not clear to me that when a well-typed
> expression does not diverge, its value is not "wrong".
>   
Every 6 months or so, I tell Stephen he should write up a formalization 
of Aldor's type system, and prove the usual Progress and Preservation 
theorems for it. 

Jacques