Modular Type Systems

点击翻译按钮获取中文摘要

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.