SoD-HCER Semantics Based System Design Using Omega

摘要：Tim SheardPortland State UTITLE：使用Omega的基于SoD-HCER语义的系统设计提案者的先前工作包括编程语言Omega的原型。Omega支持无限层次的计算级别：值、类型、种类等。所有更高级别的计算都是通过缩小来执行的。每个级别的术语按下一级别的术语分类。因此，值是按类型分类的，类型是按种类分类的，等等。保持严格的阶段区分--在级别“n”的术语的分类不能依赖于在较低级别的术语。利用Curry-Howard同构-该提案的影响是，设计的规范，程序的实现，以及程序对设计的遵守情况的检查以一种连贯的方式捆绑到一个单一的正式系统中。该提案的工作使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.