SoD-HCER Semantics Based System Design Using Omega

TIM SeardPortland State UTITLE：基于SOD-HCER语义的使用Omega的系统设计本提出者之前的工作包括编程语言Omega的原型。Omega支持计算级别的无限层次：值、类型、种类等。值级别的计算是通过减法执行的。所有更高级别的计算都是通过缩小范围来执行的。每个级别的术语按下一级别的术语分类。因此，值按类型分类，类型按种类分类，依此类推。保持严格的阶段区分--“n”级术语的分类不能依赖于较低级别的术语。利用Curry-Howard同构来形式化程序的性质--计算级“n”的项被用作“n+1”级的项的证明.本文的论点是这种系统是一种优秀的设计语言.该提案的影响是将设计规范、程序执行和检查程序与设计的一致性捆绑到一个单一的正式系统中。提案的工作使Omega系统超越了概念验证阶段。它将为Omega添加新的功能，加强Omega的基础，研究新的应用程序，并构建更强大的实现。

ABSTRACT0613969PI: Tim SheardPortland State UTITLE: SoD-HCER Semantics Based System Design Using OmegaPrevious 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.