The primary goal of my research is to discover how to design programs, components, and programming systems and to write this down in a manner that is accessible to undergraduate students:

How to Design Programs is the first book in this series. It covers the systematic design of individual stand-alone programs, mostly in the spirit of functions that consume inputs and produce outputs. These functions are either launched via a batch process, as scripts in reaction to events, or as callbacks to GUI events. -- The book appeared with MIT Press in 2001. A revision is in the planning stages. The additional material in HtDP+ suggests what this revision will look like.

How to Design Classes is the second book in this series. It covers design of re-usable components: classes, interfaces, libraries of classes, etc. in the context of object-oriented programming in class-based languages. -- The book draft is in the testing and revision phase.

In support of my research, I founded PLT, a loosely coupled group of researchers, who jointly develops PLT Scheme and uses it as an infrastructure platform for separate and joint research.

My current individual research projects usually support both my "personal mission" project as well as PLT Scheme:

Behavioral Software Contracts Jointly with Robert Findler (U Chicago), I am investigating the nature and pragmatics of software contracts. Roughly speaking, a contract is a loose, executable specification of a "module" or "component" boundary. It is occasionally possible to verify such contracts with theorem provers but more often they are monitored at run-time. When a violation of a contract is discovered, it is important that the monitoring system pinpoints the guilty party and explains how the party broke the contract. We call this blame assignment and consider it an integral part of a contract system.

With Carl Eastlund (and formerly Dale Vaillancourt), I am investigating the use of the ACL2 theorem prover as a tool for verifying some contractual information about a module interactively.

To this end we have developed Dracula a supplement for DrScheme, in which programmers can write ACL2 programs (extended with GUI code), test, run, and explore the program's behaviors, and then connect to the theorem prover to establish claims as theorems. In the near future, we intend to equip Applicative Common Lisp with modules and other constructs found in modern functional programming languages.

We have used Dracula to teach symbolic logic in a freshman course at Northeastern University with the goal of synthesizing students' programming and logic experience (details). Rex Page is using Dracule at the University of Oklahoma for a year-long Software Engineering course.

From Scripts to Typed Programs Many programs come into existence as "quick and dirty" scripts, grow up, and become large programs and sometimes large systems. This evolution demands support. Since scripting languages are typically untyped, scripts often contain hidden bugs that a type system may catch. Furthermore, the lack of types also is a gap in the "self documentation" of programs, making it increasingly difficult to maintain them. I therefore plan to explore an incremental or evolutionary approach to design that helps programmers transfactor scripts into typed programs.

After years of exploring a soft typing approach (see the dissertations by Mike Fagan, Andrew Wright, Cormac Flanagan, and Philippe Meunier) I am now exploring the construction of explicitly statically typed languages that are syntactically like scripting languages.

As a first step, Sam Tobin-Hochstadt has developed Typed Scheme, a version of PLT Scheme's core with an "occurrence type system". Next we will develop a cross-language refactoring tool that assists programmers with the task of translating one module in a program system from the untyped language into the typed one. A joint paper at the Dynamic Languages Symposium lays out the theoretical framework for this research.

Shriram Krishnamurthi (Brown) is working on a related project with Guillaume Marceau and Arjun Guha.

Interface-Oriented Programming This project is in the early stages and is a follow-up project to my 2004 ECOOP keynote. The goal is to explore the ubiquitous use of interfaces in an object-oriented setting. Richard Cobbe and Carl Eastlund are exploring different aspects of this idea, scanning existing code bases and exploring ideas to overcome difficulties with the addition of interfaces.

Design via Macro Languages For the past couple of years, Ryan Culpepper and I have investigated various aspects of PLT Scheme's macro systems. The investigation is part of a long-term program to harness the power of macros and to bring them into the mainstream of software engineering. See the papers in Dr Dobb's journal, co-authored with John Clements (CalPoly), Robert Findler, Matthew Flatt (U Utah) , and Shriram Krishnamurthi. Also see Matthew's ICFP paper on modules and macros.

Properly used, macros allow programmers to introduce syntactic abstractions that help express solutions in an extremely concise manner. In order to make macros truly useful, we need (1) mechanisms for expressing and controlling what they do and (2) tools for debugging them. In response, Ryan Culpepper has developed a contract system for macros and a macro debugger for PLT Scheme. A third project aims to turn PLT macros into a platform for implementing embedded and domain-specific sub-languages. See our joint papers at GPCE and the Scheme workshops.

Semantics On and off, I am working on the improvement of my semantic frameworks, usually in response to external questions such as how to model a certain feature in an evaluation context rewriting semantics. For this coming fall, Robby, Matthew and I are organizing a PLT Redex workshop on the framework.

Along those lines, Carl Eastlund has developed a novel framework for formulating the semantics of object-oriented languages and a tracing tool for displaying the execution behavior of class-based programs in PLT Scheme.

Matthew Flatt, Robert Findler, and I have also just published a paper on the semantics and pragmatics of the PLT Scheme class system (ASPLAS 2006) and a paper on the semantics and pragmatics of delimited functional continuations (ICFP 2007).