Modular Type Systems

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

CCR-9912352 Pierce, Benjamin C. University of Pennsylvania Modular Type Systems This project explores the use of FEATURE-BASED COMPOSITION to address issues of MODULARITY in the design, implementation, and formal analysis of type systems and related deductive systems. The ultimate goal is to build and disseminate a "type system designer's workbench" named TinkerType: a conceptual framework, tool, and component library supporting the design and analysis of type systems. It will include a substantial library of ``type system components'' covering a wide range of familiar typed lambda-calculi, as well as a tool for assembling from these components both formatted mathematical specifications and executable implementations of systems. More ambitiously, we intend to incorporate modularized proofs of properties such as soundness and decidability in the form of fragments of proof script for a mechanical proof checker. Potential applications of TinkerType include experimentation with new type systems in the form of typed lambda-calculi, as well as structured presentations of families of typed assembly languages, object calculi, etc. Moreover, the proposed mechanisms for statically checking the reasonableness of particular combinations of features are relevant to other feature-based approaches to constructing systems (for example, using the aspect- or subject-oriented programming languages being designed at Xerox or IBM or the microprotocol approach to distributed systems advocated by the Ensemble project). TinkerType is also a crucial enabling technology for a planned textbook on type systems.