Modular Type Systems

作者声明：Benjamin C.宾夕法尼亚大学模块化类型系统这个项目探讨了使用基于特征的组合来解决类型系统和相关演绎系统的设计，实现和形式分析中的模块化问题。 最终目标是构建和传播一个名为TinkerType的“类型系统设计者工作台”：一个概念框架，工具和组件库，支持类型系统的设计和分析。 它将包括一个基本的“类型系统组件”库，涵盖了广泛的熟悉的类型化可编程演算，以及一个工具，用于从这些组件组装格式化的系统规范和可执行的系统实现。 更雄心勃勃的是，我们打算将模块化的proofscript的片段的形式，如健全性和decidability的财产证明的机械证明检查。 TinkerType的潜在应用包括以类型化的汇编演算的形式进行新类型系统的实验，以及类型化的汇编语言、对象演算等的结构化表示。此外，所提出的用于静态检查特定特征组合的合理性的机制与其他基于特征的构造系统的方法相关（例如，使用Xerox或IBM设计的面向方面或面向主题的编程语言，或Encore项目倡导的分布式系统的微协议方法）。 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.