Paul Hudak - US grants

Reasoning about the operational behavior of programs written in languages whose parallelism is implicit can be difficult. This is true for purely functional languages, logic programming languages, and even imperative languages such as Fortran (when used with a vectorizing compiler). Research is proposed to study formal methods for expressing the operational semantics of parallel (and in particular functional) programs. More specifically, an investigation of the suitability of pomsets for this purpose is proposed. A symbiotic goal is the use of the formal tools to reason about and guide the design of meta- linguistic devices (such as annotations) to refine operational behavior. The research includes addressing deficiencies in previous pomset semantics; applying pomsets in new operational setting; the development of a notion of systems semantics to capture program, compiler, and machine; and the development of abstraction techniques to allow compile-time inferencing of operational behavior.

9404786 Hudak This project is in the area of programming language design and implementation. The project will develop new methodologies and tools for the design and implementation of domain specific languages (DSL). The project will apply the following ideas to the embedded language design. Extensible Language Design. Since a large portion of every language design effort is concerned with the design of the syntax, and other minor issues such as conditional statements, boolean and arithmetic operators, the project will investigate the use of generic syntax for the design of DSL's. The idea is to extend the generic syntax in a modular fashion to meet the needs of specific domains. Rapid DSL Realization Using Partial Evaluation. In order to develop DSL compilers quickly, the project will explore the use of partial evaluations. Although the resulting compilers will be less efficient than hand-crafted compilers, they will be constructed quickly and automatically, and they are provably correct with respect to the interpreter specifications. First-Class Tools. The project will apply the methodologies developed by the PI for specifying language tools such as debuggers and profilers, to the development of tools for DSL. ***

9900957 Hudak, Paul
Functional Reactive Progamming, or FRP, is an approach to programming hybrid systems in a declarative style using two particular abstractions: a continuous (functional) model of arbitrary behaviors, and a discrete (reactive) calculus for user and process interaction. FRP is a generalization of the fundamental ideas underlying two domain-specific languages that we have previously worked on: Fran, a language for functional reactive graphics and animation, and Frob, a language for functional robotics. We believe that FRP can provide a unified framework for rapidly and reliably creating hybrid software systems ranging from simple behavioral loops to large systems involving complex control strategies and multiple interacting modules. The objectives of this research are to further develop the ideas in FRP, study the principles underlying FRP, and explore ways to analyze, transform, and ultimately implement, domain-specific languages based on FRP. The research will emphasize the use of techniques common in the programming language semantics community. Amongst the issues to be investigated are: denotational as well as operational semantics for a small reactive language with continuous behaviors, an implementation synthesized from first principles (i.e. correct with respect to a specification), and practical ramifications of using numerical methods to simulate continuous behaviors.

Techniques such as program generation, partial evaluation, just-in-time compilation, and run-time code generation respond to the need for general purpose programs which do not pay unnecessary
run-time overheads. The thesis of this project is that a uniform, principled, high-level, and practical view of these diverse techniques is possible through multi-stage programming, a novel paradigm for the development of maintainable, high-performance software. The key idea in multi-stage programming is the use of simple, high-level annotations to allow the programmer to break down the cost of a computation into distinct stages.

The goal of this proposal is to demonstrate that the theoretical machinery that has been developed for multi-stage programming can be put to work. This project will involve the development of compilers
of multi-stage programming languages, addressing both practical and theoretical problems that arise in the development of such systems, and using these compilers in interesting applications ranging from dynamic programming algorithms and rewriting systems to implementations of domain specific programming languages.

Taha, Walid
CCR-0205542
"ITR: A Framework for Rapid Development of Reliable Robotics Software"

Robots are entering daily life. Commercially available systems are
delivering medication to patients in hospitals, mowing lawns, vacuuming
floors, and finding wide applications in the entertainment industry. In the future, they will play a more substantial role in areas such as space exploration, health care, and search and rescue. But as
these applications grow, so does the complexity of these robots, making
the reliability of their software and the productivity of their
programmers a priority. It is not clear that current techniques for
programming robots are sufficient for building systems that are orders of magnitude more complex than the ones available today. The vast majority of programming methods in current use focus on high-level planning and task and behavioral aspects. By contrast, there are no widely-accepted specialized software processes or programming languages for the integrated development of robotics applications.

This project explores the impact of state-of-the-art programming languages techniques in a small-scale robotics setting. The project applies domain-specific languages methods and automatic program generation techniques. The framework exploits core technologies such as multi-stage programming with simple, high-level annotations
to avoid unnecessary runtime overheads yet provide a natural and algorithmic approach to program generation, where generation occurs in a first stage, and the execution of the synthesized program occurs in a second stage. Because (even when the final goal is embedded software) the first stage does not need to be resource-bounded, conventional programming techniques can be used.

The challenge, then, becomes ensuring that the generated programs are suitable for execution on an embedded platform. Multi-stage languages already provide significant safety guarantees. For example, a program generator written in such a language not only is type-safe in the traditional sense, but we are guaranteed that any generated program will also be type safe. This provides a noteworthy degree of assurance about the quality of the generated code. But like most traditional high-level programming techniques, multi-stage programming was designed to satisfy functional requirements rather than operational ones, and existing multi-stage languages do not provide any guarantees about the behavior of programs in the presence of bounded resources. The focus of this project is ways to address this problem by strengthening
``traditional'' multi-stage type systems using a number of state-of-the-art techniques from type theory and functional reactive programming (FRP) to create resource-aware multi-stage programming. Linear and alias types (in conjunction with dependent typing) will be used to ensure space-boundedness, new typing techniques are used to ensure time-boundedness, and signals and behaviors from FRP allow for a natural style of reactive programming.

CCR-0306046
Functional Hybrid Modeling
Henrik Nilsson, Paul Hudak, and John Peterson
Yale University

This project integrates functional programming with non-causal hybrid modeling into a powerful, strongly typed, fully declarative modeling and simulation language, combining the strengths of each paradigm. The work on Functional Reactive Programming has demonstrated how causal modeling in a functional setting allows highly dynamic hybrid systems to be described. However, non-causal modeling is instrumental in making large-scale modeling manageable, and the associated symbolic and numerical methods are essential for efficient and numerically sound simulation.

The goal is a language that provides modeling capabilities beyond the current state of the art while allowing efficient simulation, and is semantically rigorous to facilitate modeling, reasoning about models, and catching certain modeling errors. Central research areas include the semantics of integrated functional hybrid modeling; reconciling the implementation techniques of the hybrid simulation world with those of modern declarative languages and dynamic code generation; and a type system tailored to physical modeling incorporating recent ideas from type theory to enhance the safety and robustness of the models.

The project will facilitate designing and understanding complex systems in the real world by providing users with a highly expressive modeling language that is suitable for programming a broad range of modeling and simulation applications.

Robots are becoming increasingly common in, and important to, many commercial, industrial, and military applications. This project focuses on humanoid robots, which are becoming increasingly useful as they advance in sophistication, because they can perform in environments engineered specifically for humans, and because they make it easier for humans to interact with automation. This project focuses specifically on how to program humanoid robots; i.e. how to program their movements and interactions as easily and as effectively as possible. The focus is not on developing new algorithms for robot movement or sensing. Rather, once an algorithm is in hand, how does one program a robot to walk, wave its arms, clap its hands, or pick up an object? How does one do so in a high-level way that is devoid of unnecessary detail, yet is expressive enough to capture all desirable movements and interactions?

The core of this effort is the design of a domain-specific language called "Dance" that is highly abstract, easy to use, yet has enough expressive power to describe a wide range of useful robot movements. Dance incorporates ideas from the PI's previous work on domain-specific languages for computer music, computer animation, and software-enabled control. For example, Dance uses declarative event-based reactivity to give a robot the ability to respond to its environment (through tactile, aural, and visual sensors), to its own body (such as interactions between limbs), and to internal programmatic events (timers, remote messages, user commands, and so on). Innovative language research makes behaviors the objects of computation in Dance, which enables programs to abstract over (aggregate) action sequences and evaluate interactions of such sequences. The language is also amenable to formal reasoning based on a formal algebraic semantics. It is possible to prove crucial run-time properties of Dance programs based on the axioms of this algebra. The proposed work also includes a programming environment called "Dance Studio" that has the ability to simulate and thus visualize a running Dance program, enabling a programmer to dynamically debug her programs prior to full robot deployment.

Dance language research pioneers a control programming concept that is relevant for many applications in which complex, aggregate system behaviors or maneuvers are required, and in which such behaviors must be coordinated and assured. The research is part of, and supports, a broader agenda at Yale to create "socially adept" robots. Building a machine that can recognize social cues from a human observer allows a more natural human-machine interaction style, creates possibilities for machines to learn by directly observing untrained human instructors, and expands on the growing capabilities of robotic systems. Such social machines can be used as investigative tools to study many aspects of human social development. For example, a robot that is capable of perceptually identifying social cues can be used to provide a quantitative metric of social response. This metric may be a useful diagnostic tool for social development disorders such as autism. In fact research on the use of humanoid robots to diagnose and treat autism is being conducted in the broader scope of Yale's humanoid robotics program.

Some of the most exciting cyber technologies on the research horizon involve sophisticated digital systems that interact with the physical world. Examples include remote surgery, physical manipulation of nano-structures, autonomous (ground and air) vehicular travel, and space and terrestrial exploration. Because such applications interact directly with the physical world, it is imperative their physical safety be assured. This project is developing a comprehensive formal framework for producing controllers for cyber-physical systems, with machine checkable proofs of their physical safety. The project brings together ideas from control theory, language design, program verification, program generation, software engineering, and real-time and embedded systems to build a framework that can be applied to challenging applications. The framework promotes an efficient, rigorous engineering process for producing embedded controllers, incorporating explicit models not only of the controller itself, but also of the physical context in which it operates, the required stability conditions, the platform on which it will run, and the associated real-time constraints. The results of the project are being demonstrated and evaluated in the context of a tele-surgery application. This application is currently being developed at the Mechatronics and Haptic Interfaces Lab in the Mechanical Engineering Department at Rice University.

This research focuses on developing a new programming methodology to dramatically improve the quality and dependability of software-intensive systems. The key to this effort is an effective integration of domain-specific languages (DSLs) and formal program verification, two well-known technologies that have been used extensively on their own, but mostly in isolation of one another. DSLs make it easier to write complex software for specific application domains, but they often lack rigorous semantics, making it difficult to formally specify and reason about the resulting programs. Existing program verification systems, on the other hand, usually rely on a single unified logic (e.g. Hoare logic) or type system, which cannot support the diversity of components in typical software-intensive systems. By combining the two methodologies, the PI intends to resolve both of these shortcomings. More specifically, the PIs propose to develop a new DSL-centric certified software design methodology that will elevate existing DSL practice into a rigorous software development methodology that allows program verification to scale effectively to large software systems. The proposed research will impact the software engineering community and make it possible to build software more quickly, and with higher assurance of correctness, than previously possible.

Functional Reactive Programming, or FRP, is a declarative programming paradigm based on two fundamental abstractions: a continuous (functional) modeling of time-varying behaviors, and a discrete (reactive) calculus of user and process interaction. FRP provides a novel and effective approach to solving problems in which there is a combination of both continuous and discrete entities such as found in computer animation, robotics, control systems, GUIs, and interactive multimedia. FRP?s broader impact is seen in its adoption by several other research projects, and its use in several applications different from those at Yale. The proposed work will strengthen these existing projects, and further broaden the applicability of FRP. The proposed improvements in implementation will make FRP more suitable for compute-intensive applications, such as interactive 3D graphics and real-time audio processing. It will also benefit the modeling and simulation community, which often uses declarative approaches to specifying and solving problems.

Previous research at Yale helped to establish the foundations of FRP, and demonstrated its utility in several application domains. Despite this preliminary success, more work is needed to make "FRP for real." That is, to develop a system that facilitates writing natural and concise descriptions of reactive behaviors, responds well enough to satisfy most common real-time constraints, reifies real-world objects as first-class signal functions, runs efficiently through program optimization and parallel execution on multicore architectures, and has been validated in a real-world application domain, specifically audio signal processing. The proposed research will advance the overall FRP methodology in three areas: Language Design (type system extensions to capture resource constraints, a redesign of the mediation between the discrete and continuous, and a better syntax to capture the essence of FRP); Language Implementation (program optimizations, multicore execution, asynchronous sub-processes); and Validation and Testing (with a focus on real-time audio signal processing).