Previous work of the proposers includes a prototype of the programming language Omega. Omega supports an infinite hierarchy of computational levels: value, type, kind, etc. Computation at the value level is performed by reduction. Computation at all higher levels is performed by narrowing. Terms at each level are classified by terms at the next level. Thus values are classified by types, types are classified by kinds, etc. A strict phase distinction is maintained -- the classification of a term at level "n" cannot depend upon terms at lower levels. Properties of programs are formalized by exploiting the Curry-Howard isomorphism -- Terms at computational level "n", are used as proofs about terms at level "n+1".
The thesis of the proposal is that this kind of system makes an excellent design language. The impact of the proposal is that the specification of designs, the implementation of programs, and the checking of adherence of programs to designs are bundled in a coherent manner into a single formal system.
The work of the proposal carries the Omega system beyond the proof of concept stage. It will add new features to Omega, strengthen Omega's foundations, investigate new applications, and build a more robust implementation.
