CSD Home | SCS Home



Research Areas - Programming Languages Research in the Computer Science Department at Carnegie Mellon


CSD faculty: Guy Blelloch, Steve Brookes, Karl Crary, Seth Goldstein, Robert Harper, Frank Pfenning, Andre Platzer, John Reynolds, Jeannette Wing

Affiliated Faculty: Jonathan Aldrich (ISR), Anupam Datta (ECE), Richard Statman (Math)

Founded by Dana Scott in 1981, the Programming Languages faculty at Carnegie Mellon are widely recognized as world leaders in the theoretical foundations, practical implementation, and application of programming languages. Our research is concerned with a comprehensive science of programming that encompasses not only language design and implementation as ordinarily conceived, but which also encompasses specification, verification, implementation, evaluation, and validation of programs. Our thesis is that programming is fundamentally an explanatory activity, which requires that a program be codified in a form that not only supports execution on a computer, but also manifests its design so that they can be understood by its developers and maintainers, and subjected to mechanical verification and validation. Such rigorous explanations demand that we develop formal languages with precise semantics that provide a direct link to the running code. But mere precision and clarity are not enough, we must also ensure practicality. To achieve this we must use our tools to build software systems, and evaluate their utility both analytically and empirically. Consequently, our work encompasses a broad spectrum of research, ranging from abstract theories of programming concepts to large-scale implementations of these ideas in working software systems.

It is precisely this broad scope of investigation that distinguishes us from our competitors. Over the last two decades we have repeatedly demonstrated that fundamental theory is essential for building robust and reliable systems, and that enduring and elegant theories arise from meeting the demands of building such systems. Examples include our work on FoxNet, a composable suite of networking protocols (Harper, Lee); Twelf, a logical framework and theorem prover that permits precise formalization of languages and logics, and semi-automatic proofs of their properties (Pfenning, Harper); PCC and TIL, the first certifying compilers, which generate object code equipped with a machine-checkable proof of safety (Lee, Harper, Crary); separation logic, which permits compositional reasoning about programs that make use of delicate pointer manipulations (Reynolds, Brookes); cost semantics and provable implementations of parallel languages (Blelloch); self-adjusting computation as a design technique for dynamic algorithms (Blelloch, Harper); type systems for modular programming (Harper, Crary); and ConCert, a system for developing and deploying grid-computing applications in a trustless environment (Crary, Harper, Lee, Pfenning).

A common thread in these examples, as in much of our work, is the sophisticated combination of fundamental theoretical advances with disciplined engineering to build powerful new tools and develop novel applications. We contend that many of these advances could not have been achieved by any other means. Whereas there is a well-established tendency in academic computer science to distinguish theory and systems as separate research areas, we are, on the contrary, committed to an integrated view of computer science as a coherent discipline that makes equal use of theoretical and empirical methods to solve practical problems. In our work we prove theorems and report numbers, often in the same paper!

Another theme is the commitment to clarity and elegance as the defining characteristics of good theories and good systems. We impose on ourselves the discipline of finding solutions that do more than "just work'', but moreover are works of art that can be appreciated for their intrinsic merits, independently of their extrinsic applicability. The simplicity of the LF logical framework, the elegance of the FoxNet protocol interface, and the graceful manner in which separation logic captures the subtleties of pointer structures exemplify our ideals. We contend that the demands placed on modern software systems imply that we can no longer afford the luxury of an ugly hack. If a program or a theory is not beautiful, no one could understand it well enough to know that it is right, nor would use it to meet such demands.

Others have put forth similar convictions, but few have enjoyed the success that we have attained in a little more than two decades. What has enabled us to succeed where others have failed is that we have employed a "secret weapon'' --- the realization that type theory, logic, and semantics provide a single, vertically integrated foundation for a science of programming that spans the range from low-level machine languages to high-level programming languages with powerful type and specification systems, and encompasses not only the executable code itself, but also the reasoning that informs its design and correctness. The power of this perspective is by now apparent to everyone, and is by now the central organizing principle of the field. This shift is largely a consequence of the scientific process of publication and review, but is also due, in part, to our success in placing our graduates at top universities and laboratories, including Greg Morrisett (Cornell, Harvard); George Necula (University of California at Berkeley); Olin Shivers (Georgia Tech); Benjamin C. Pierce (University of Pennsylvania); Perry Cheng (IBM Yorktown); David Tarditi (Microsoft Research); Carsten Schuermann (Yale, ITU Denmark); Lars Birkedal (ITU Denmark); Christopher Stone (Harvey Mudd); Leaf Petersen (Intel); Umut Acar (TTI Chicago); Derek Dreyer (Max Planck Institute).

Our success in advancing an integrated view of Computer Science encourages us to take on even greater challenges, and opens up many new possibilities for us to explore. We envision that future languages will have fully formal definitions with fully checked proofs of their safety and security properties as a matter of course. Currently available tools, such as Twelf, are already expressive enough to make this feasible for realistic languages such as the POPLMark Challenge (posed by Pierce and others at UPenn) and Standard ML. Research is already under way on enriching their expressive power and convenience to make the task simpler, more modular, and easier to maintain and evolve. In particular we envision the development of logical frameworks that support a more direct and natural representation of shared state and of concurrent interaction than is currently feasible.

Our experience with the design and implementation of certifying compilers emboldens us to assert that in the future all compilers will be certifying compilers that will make use of expressive type systems in intermediate and object code, as well as source languages. Compilers are very complex software systems that are notoriously difficult to maintain and evolve. Certification permits a degree of self-checking within a compiler that greatly increases the modularity of the compiler itself, and correspondingly vastly enhances our ability to make significant changes to a component without disrupting crucial invariants assumed by other components. Moreover, certifying compilers generate object code that carries with it a machine-checkable proof of safety and security properties, eliminating or greatly reducing the need to rely on the correctness of a compiler to ensure the well-behavior of a binary executable.

The effectiveness of type systems for improving code quality, reducing development costs, and enhancing maintainability of software is by now beyond dispute. We believe that the trend toward languages with increasingly expressive type systems will accelerate, and that the demands for type systems of ever-greater expressive power will increase as developers become accustomed to their use. In the near future we expect to see type systems that are capable of expressing, and mechanically enforcing, crucial data structure and protocol invariants across module boundaries. In the longer term we expect a convergence of type systems and specification languages to achieve a complete integration of these important tools for reasoning about program behavior. There is every reason to pursue these goals aggressively, and we are optimistic that the foundation of tools and theories that we have developed will serve as a solid basis for this work.

      CSD Home   Webteam  ^ Top   SCS Home