Presidential Young Investigator Award (Computer Research): Programming Language Features Within a Type-Theoretic Frame-work

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

Formal methods, as traditionally used in the mathematical analysis of logic or natural language, have proven useful in several branches of computer science. Here the interest is in using formal systems to study contemporary programming languages, with general aims towards understanding current concepts more precisely, and using this understanding to design simpler and more expressive languages for the future. As a means for exploring pragmatic issues, it is planned to assemble a "programming language work bench" comprising an interactive, programmable front-end, such as the Cornell Synthesizer Generator, and a standard incremental code generator. In another direction, logical and linguistic problems related to database and knowledge representation systems will receive attention. One problem in the study of programming languages is the lack of standard terminology, which reflects a great diversity among computational metaphors. For example, Smalltalk is presented using a metaphor of "objects" and "messages", while Prolog is often explained as program synthesis from specifications. The differences between approaches makes it difficult to compare or combine features of different languages, or to evaluate the hazards and benefits of such combinations. Various typed notations for describing computable values, often called "type theories" or "typed lambda calculi" have attracted increasing attention in recent years. These systems are generally simply defined, without ad hoc syntactic restrictions related to implementation considerations, and sufficiently expressive to serve as intermediate languages for both theoretical analysis and practical implementation. Early work on denotational semantics helped establish a connection between simple typed lambda calculus and the Algol-like languages, while more recent work has both extended this view to languages with polymorphic functions and data type declarations, and refined the approach to be more practically useful. It is planned to continue research into the mathematical properties of typed lambda calculi, and efforts to apply these systems to programming language analysis and design. In particular, it is planned to develop a modern course on programming language theory and its application, and use the framework of typed lamdga calculus to analyze contemporary language features such as class hierarchies and method inheritance.