Modular Type Systems

CCR-9912352皮尔斯，本杰明C.宾夕法尼亚大学模块化类型系统这个项目探索了在类型系统和相关演绎系统的设计、实现和形式化分析中使用基于特征的组合来解决模块化问题。最终目标是构建和发布一个名为TinkerType的“类型系统设计者工作台”：一个支持类型系统设计和分析的概念框架、工具和组件库。它将包括一个“类型系统组件”的实体库，它涵盖了广泛的熟悉类型的lambda演算，以及一个从这些组件汇编格式化的数学规范和系统的可执行实现的工具。更雄心勃勃的是，我们打算将属性的模块化证明，如可靠性和可判断性，以校样脚本片段的形式用于机械校验器。TinkerType的潜在应用包括对类型化的lambda演算形式的新型系统的实验，以及类型化汇编语言、对象演算等的结构化表示。此外，提出的用于静态检查特定特征组合的合理性的机制与其他基于特征的构建系统的方法相关(例如，使用Xerox或IBM正在设计的面向方面或面向主题的编程语言，或由Ensymble项目倡导的分布式系统的微协议方法)。TinkerType也是计划中的关于类型系统的教科书的关键使能技术。

CCR-9912352Pierce, Benjamin C. University of PennsylvaniaModular Type SystemsThis project explores the use of FEATURE-BASED COMPOSITION to addressissues of MODULARITY in the design, implementation, and formalanalysis of type systems and related deductive systems. The ultimategoal is to build and disseminate a "type system designer's workbench"named TinkerType: a conceptual framework, tool, and component librarysupporting the design and analysis of type systems. It will include asubstantial library of ``type system components'' covering a widerange of familiar typed lambda-calculi, as well as a tool forassembling from these components both formatted mathematicalspecifications and executable implementations of systems. Moreambitiously, we intend to incorporate modularized proofs of propertiessuch as soundness and decidability in the form of fragments of proofscript for a mechanical proof checker. Potential applications ofTinkerType include experimentation with new type systems in the formof typed lambda-calculi, as well as structured presentations offamilies of typed assembly languages, object calculi, etc. Moreover,the proposed mechanisms for statically checking the reasonableness ofparticular combinations of features are relevant to otherfeature-based approaches to constructing systems (for example, usingthe aspect- or subject-oriented programming languages being designedat Xerox or IBM or the microprotocol approach to distributed systemsadvocated by the Ensemble project). TinkerType is also a crucialenabling technology for a planned textbook on type systems.