Note: Some of my papers are linked in multiple categories below, while others aren't linked at all. If you want to find a particular paper, go directly to the chronological list of all papers instead.
My research program studies the following areas:
Modern end-user applications are fundamentally interactive. Yet traditional programming language design and semantics have failed to capture the needs and subtleties of such systems.
My focus has been on the nature of Web software, which proves to be surprisingly subtle and leads to innumerable errors. On the programming front, I am interested in undoing the constraints that the Web's statelessness imposes on the programmer, either through better Web servers [link] or via compilation techniques [link] based on continuation-passing style (CPS). Unfortunately, while it is natural to employ CPS, the transformation has many disadvantages. We have therefore devised a better strategy, which can also be used to implement continuations atop uncooperative virtual machines (such as the JVM) and intermediate languages (such as MSIL) [link].
Moving past specific programming techniques, what is the essence of Web interactions? We have constructed a core calculus that enables us to reason about such computations [link]. Furthermore, given that errors will exist independent of language (better languages simply lead to more interesting errors), we have built a model checker (which exploits our calculus) to take into account the myriad of problems introduced by end-user actions [link]. We are also studying the safety and availability of data in these applications [link].
Many of these papers refer to my conference management software, Continue (read an early paper on it). The current state of conference management software is parlous at best. I have heard from several quarters that one reason for this is that there isn't any research in the topic. I like to think my research demonstrates how false this claim is.
The Web is, of course, just a special case of an interactive system (though an especially interesting and important one). Can we devise better programming languages to build other kinds of interactive systems, such as GUIs? In some special cases, we can map the needs of GUIs back to our insights from the Web [link].
For traditional desktop applications, my student Greg Cooper is working on a functional reactive language called FrTime [link] that is designed to support interactivity from the bottom up. A particularly compelling use of FrTime is in the context of scriptable debugging [link]. We have also studied the principled adaptation of object-oriented libraries to FrTime [link].
Software engineers often precede language theoreticians. The past decade has seen a spate of proposals for new forms of software composition, with names like ``mixin layers'', ``hyperslices'', ``aspects'', and so on. These proposals have emerged from a concrete need felt in the process of trying to build, deploy, maintain and re-deploy software systems. While programming language theory has fallen behind these results, the semi-formal presentations of these modularity mechanisms offer enough basis to enable progress on other fronts.
While each new development technology is exciting, I believe we cannot consider one mature until it provides comprehensive support for software development: programming, testing, editing, compilation, verification, etc. While I have investigated many of these issues, in this slice of work I've focused on formal verification. Of the many verification techniques, I have found model checking an especially good fit with many of the properties we have encountered in our case studies.
A recent position paper puts this research program in perspective, emphasizing the challenges that led to the work listed below.
Our initial work [link] presented a model for model checking product-line systems built out of components. We observed that the mode of composition in these systems is sequential, and thus different from that in the traditional verification literature, forcing the need for new techniques. We showed, also, how to support a limited (and apparently sufficient) form of parallelism. Our preliminary experiments [link] validated the claimed benefits.
Despite this success, we noticed a weakness in the handling of both data and propositions in this modular context. This led to the adoption of much a more complex verification technique (three-valued model checking). While less elegant, the work proved to be highly effective [link].
Our dissatisfaction with the complexity of the three-valued approach led us to consider a different line of attack. The insight we gained is that thinking of the problem as one of ``verification'' is incorrect because one module, on its own, is rarely ever right or wrong. Instead, each module simply imposes constraints on the rest of the system, and error detection is a matter of finding irreconcilable constraints [link].
Meanwhile, we have also been extending our earlier results to more flexible linking languages, especially those reflecting the forms of dynamic composition supported by aspects. This leads to a different set of challenges. We have had preliminary success in this dimension as well [link]. Because of the assumptions this makes, however, though this work should more rightly be called ``incremental'', rather than ``modular'', verification.
Hackers precede language theoreticians, too. We are seeing a flood of novel and innovative programming languages within various specific domains. Because they arise out of specific needs, however, they are often designed by people without traditional language design expertise, and implemented by people without traditional programming environment expertise. As a result, they present numerous opportunities for people with programming language analysis experience. What makes these languages exciting is that they are actually being used by developers, so results can both be deployed rapidly and will quickly garner useful feedback. Here are two examples.
I am especially fond of spreadsheets. Their constrained shape seems to be a structuring aid in many domains; in any case, it provides automatic naming, which reduces some of the (initial) burden on the spreadsheet author. The dominant spreadsheet, Excel, is rich in features but unfortunately poor in support for spreadsheet validation. We have, building on prior work, developed a novel type system [link] whose types are the names of spreadsheet headers. Furthermore, because most spreadsheet data are numeric, we have also built a system for checking units [link].
I have also been working on two problems related to XACML, a standarized declarative language for access-control specifications. The first problem is the validation of policies against a set of known properties. Moreover, developers often do not have properties; all they have is a prior version of the policy that seemed to work correctly, and a new version with some changes applied. To support this important use-case, we also implement change impact analysis, which summarizes the semantic (as opposed to syntactic) changes to a policy. Happily, the outcome of this analysis can itself be treated as a source for verification, enabling a very elegant, lightweight formal methods technique [link].
Computer scientists have traditionally considered the program source as a static entity and the program's behavior as dynamic. In fact, the program source has never been static, constantly evolving in response to errors and changing requirements. The easy availability of multiple versions of a program through the agency of public version-control repositories has enabled an exciting new branch of program analysis: the treatment of the program source as a dynamic entity. One of our projects analyzed the source to find the impact of each program relative to the program's decomposition by feature [link]. In addition, our work on XACML policy analysis also treats the access control specification as an evolving entity, providing support for studying this evolution through change impact analysis [link]. These efforts take a much more archeological approach to program growth than my older work on black-box extensibility [link, link, link].
I was one of the initial designers and developers of DrScheme [link]. DrScheme has featured numerous innovations including a static debugger [link], multiple levels of presentation for one programming language [link], advances in macro systems [link], and much more. More recently, DrScheme has served as an implementation base for various aspects of our work on interactivity.
Any concern for a programmer's needs must take into account tools for debugging. Directly or indirectly, most of my work on programming environments, type systems and verification is related to debugging. I have also investigated debugging in the traditional sense. We have studied the question of applying potential invariants to identifying the location of a program's fault [link] with, however, mixed results. More fruitfully, we have studied the design of a programming language for scripting a debugger; this is a showcase for our work on language research for interactive software [link].