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

CSD faculty: Guy Blelloch, Steve Brookes, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning, John Reynolds, Richard Statman (Math)

Founded by Dana Scott in 1981, the Principles of Programming (PoP) 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).

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); Umut Acar (TTI Chicago).

Various research projects and initiatives provide the scientific and funding context for collaboration within the group, with other faculty within CSD and SCS, and at other universities and research laboratories. Collaborations within the PoP faculty include the ConCert Project (NSF ITR), which seeks to develop a trust-free grid computing framework (Crary, Harper, Lee, Pfenning); the Triple Project (NSF), which seeks to enrich the expressive power of type systems (Harper, Pfenning); parallel real-time garbage collection (Microsoft Corporation), which seeks to extend automatic storage management to real-time systems (Blelloch, Harper). Broader collaborations within Carnegie Mellon include the Aladdin Project (NSF ITR), in collaboration with several faculty, on applied algorithms (Blelloch, Harper); an IRAD project (SEI) in collaboration with Edmund Clarke on extending model checking with separation logic (Lee); the Claytronics Project (NSF, DARPA, Intel), in collaboration with Seth Goldstein, on synthetic reality (Lee); a project developing compilation techniques for FPGA's in collaboration with Seth Goldstein (Crary, Lee). Externally to Carnegie Mellon, there is the Logosphere Project (NSF), in collaboration with SRI, Yale, and Cornell, on developing digital libraries of formal proof (Pfenning); and the Aladdin Project (NSF ITR), in collaboration with Princeton and Yahoo (Blelloch, Harper).

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 large fragments of the ML language. 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.

Speaking more broadly, we believe that it is time to challenge the prevalent, if tacit, assumption that we must live with low-quality, unreliable software that is prohibitively expensive to improve, much less replace. Rather than accept the status quo and try to live with it, we do better to challenge it and try to do better. It is our contention that a comprehensive approach based on the application of fundamental theory to programming practice is the best strategy for overcoming the limitations of current software systems and practices.