Programming Language research at Yale emphasizes expressive, efficient, flexible, and reliable programming environments for future information, computation, and communication systems. We approach this problem from several directions including language design, formal methods, compiler implementation, programming environments, and run-time systems.
One approach to achieving high-quality programming environments is via high-quality programming languages. Several programming languages developed at or associated with the department (in particular Haskell, Linda, and Standard ML) have achieved worldwide currency, reflecting the department’s leadership in the areas of functional programming and parallel computing.
Haskell is a purely functional programming language in which programs are written in a highly mathematical, declarative notation, facilitating the use of formal methods and its use as both a prototyping language and an executable specification language. Linda is a coordination language based on a shared and associative object memory model which has proved useful for distributed and ensemble computing; efficient Linda implementations exist on most asynchronous parallel architectures, and the system sees increasingly widespread use as a production programming vehicle.
Many application domains have distinct requirements that dictate the development of special-purpose software. Work at Yale has focused on the ultimate goal of this process: the design of domain-specific languages that capture precisely and succinctly an application domain’s underlying semantics. Research in the design, formal semantics, and implementation of such languages is underway, with applications in graphics, animation, robotics, computer vision, computer music, and general control systems. This work has led to the development of functional reactive programming (FRP), a high-level, declarative framework for specifying, prototyping, and implementing “hybrid”systems that combine both continuous values and discrete events. Of particular interest is the use of FRP in real-time and embedded systems, where resource consumption (in both time and space) is a critical issue, and must be known at compile time. For more information about this research, please visit the Yale Haskell Group’s website at http://haskell.cs.yale.edu/.
Zhong Shao’s research interest is, very broadly, on building reliable and secure computer software. The computer industry has shown explosive growth in the past thirty years. Software dependability, however, falls far behind everything else because we do not have good languages and tools that can take precise control of the ever-growing complexity in modern computer systems. During the last few years, Professor Shao’s FLINT group has been developing and applying new language-based technologies to build certified system software (e.g., OS kernels and hypervisors). Certified software consists of a binary machine executable plus a rigorous machine-checkable proof that the software is free of bugs with respect to specific requirements. A certified OS kernel is a library-based kernel but with formal specifications and proofs about all of its abstraction layers and system libraries. The FLINT group is currently working on the following three important questions: (1) Under a clean-slate approach, what are the right OS kernel structures that can offer the best support for resilience, extensibility, and security? (2) What are the best programming languages and developing environments for implementing such certified low-level programs? (3) What new formal methods we need to develop in order to support these new languages and make certified programming both practical and scalable?
On a larger scale, David Gelernter’s software ensemble research is the study of programs that are built out of many separate, coordinated activities, with an emphasis on recognizing and understanding the properties that all such systems share, versus the more widespread practice of dividing the field into intellectually disjoint sub-areas. Ensemble computing includes the study of: (1) parallel programs, which focus many computers on a single problem in order to solve it faster; (2) distributed programs, which attempt to integrate many separate, autonomous computers; (3) ensembles, which include time- as opposed to space-separated activities and which pose new research challenges in the areas of file systems and databases, and; (4) the relationship between software ensembles and naturally occurring ones, as for example in economic, biological, or physical systems. All of these areas pose both theoretical and pragmatic questions. The search for a formal definition of “coordination language,” and the development of Internet applications are new areas of focus in the software ensemble research effort.
Faculty members in the Programming Languages and Systems area are David Gelernter, and Zhong Shao.