FRANK PFENNING
Professor, Computer Science
Director, Computer Science Ph.D. Program
www

At the heart of my research lies the desire to understand the principles of programming languages. Programming languages are the key to the programming process and therefore of fundamental importance to computer science. Well-designed programming languages allow fast program development, ease software maintenance, and increase confidence in the correctness of implementations. Poorly designed programming languages lead to verbose and impenetrable programs that are difficult to debug and maintain. One of the trends in computer science has been the development of a plethora of languages, often for very specific purposes. Unfortunately, many of these languages are woefully misdesigned, because their developers were unaware of or have disregarded basic principles of programming language design. My research thus aims at discovering such principles and experimenting with them through implementations and environments.

In support of this goal, I am pursuing three interconnected threads of research. The first is the development of meta-languages which codify programming language concepts and support formal reasoning about properties of programming languages. The second is the design of expressive type systems for practical programming languages which allow more program errors to be caught at compile-time without sacrificing conciseness or efficiency of programs. The third is the application of programming language techniques in domains where they are currently undervalued, such as mobile code or robotics. In all of these I collaborate closely with colleagues and students who are not mentioned explicitly below. Please refer to my home page for recent drafts and publications.

Meta-languages. In this area my research focuses on the development of a uniform meta-language and environment which supports specification, implementation, and formal reasoning about programming languages and logics. The currently released implementation is Twelf 1.2 which embodies many of the representation and implementation techniques discovered in my research on logical frameworks. Underlying Twelf is a type theory which is used for specification, constraint logic programming, and meta-theoretic reasoning. Twelf is a significant step towards an environment for teaching and research in the areas of programming languages and logics. Current and future work on Twelf consists mainly in improving its expressive power to capture more language phenomena in a concise and natural way. There is ongoing work on a linear extension (to capture imperative and concurrent computation), an ordered extension (to capture adjacency and sequencing), and extension by constraints (to capture integers, rationals, and similar domains).

Type systems.. In this area I have concentrated on extending the expressive power of type systems to allow more properties of programs to be checked statically. Invariants which can otherwise only be stated informally can be expressed in these systems and verified by a type-checker. This provides additional machine-checked documentation, more detailed interface specifications at the module level, and allows more errors to be detected at compile-time. All these properties combine to improve programmer productivity and simplify program maintenance. Concretely, I have developed refinement types (for inductively specified properties of data representation), dependent types (for array bound and similar constraints) and modal types (for run-time code generation).

Applications. I believe that programming language research cannot exist in a vacuum---it must address problems encountered by real programmers in real applications. Whether this is the case is often difficult to assess, since at present the gap between research on advanced programming languages and programming practice is, unfortunately, very large. One way to reduce this gap is to take problems faced by programmers today in specific areas and contribute to their solution with programming language techniques. The ConCert project at CMU is an example of this, where we develop techniques for combining modularity with safety and efficiency in the context of grid computing using tools from logic and type theory.  In other research I am exploring questions of programming language design for applications in robotics and manufacturing.

semantic system; and 4) sentence-level processing and the interplay of syntax and semantics.