Today we solve computational problems using not only a diverse set of machines but also a diverse set of high-level programming languages. The main factor driving diversity in programming languages is that special-purpose languages help users solve problems in ways that, without these languages, would be too expensive or even impossible. One example is the rise of Perl and other scripting languages for rapid prototyping. Another is the advent of Java, which by providing an appropriate security model, made it safe for ordinary users to run code from untrusted, remote Web sites—helping to stimulate today's vigorous electronic commerce. In the future, we can expect to see more programming languages that guarantee important properties, such as privacy or security, for every program written in these languages. Such guarantees help boost the productivity of programmers and the reliability of the software they produce.
The benefits of specialized machines and programming languages create continual demand. But for a new machine or a new language to be successful, the ``semantic gap'' between machine and language must be bridged by suitable infrastructure. At present, this infrastructure is built by hand, at high cost. This cost blocks the programming-language community, which wants to explore new designs, but is hampered by the engineering cost of building infrastructure. The goal of my research is to find systematic, reliable, cheap ways of building this infrastructure. Reaching this goal will, among other effects, free programming-language researchers and enable more innovation in languages. To work toward the goal, I have developed infrastructure that is reusable in two dimensions: across languages and across machines. I present my infrastructural contributions in detail below, but here I highlight two: reuse of a compiler with multiple languages and with multiple machines.
Because building a compiler requires substantial effort—several years or more—making a compiler reusable with multiple languages offers a large payoff. But not just any compiler will do: to be reusable with multiple languages, a compiler must support each language's variation on features that are implemented primarily by run-time services, such as garbage collection, exception dispatch, concurrency, and security. Older compiler infrastructures have been able to ignore run-time services, because they have dealt primarily with legacy languages like C and Fortran, which require only very simple run-time services that don't need support from the compiler. But the trend in languages is to provide more and more guarantees by means of run-time services, and interactions between compilers and run-time services are growing increasingly complex. Newer infrastructures have responded to these problems by building in one implementation of each service. But one size does not fit all: language designers have definite ideas about the appropriate semantics and cost tradeoffs for run-time services, and different designers decide these questions differently. The result is that an infrastructure designed for one class of languages cannot be used to support another.
My contribution has been to show that run-time-services can be supported by means of a run-time interface, which reveals to a run-time system the important decisions made in the compiler's back end—providing the necessary support—but which avoids militating toward any particular implementation—giving the language designer the freedom to choose semantics and cost tradeoffs. For example, I have shown that a run-time interface can support accurate garbage collection for multiple languages while enabling each individual language to make different decisions about what constitutes a pointer and how to mark the layout of heap objects. And I have shown that combined with innovative control-flow mechanisms, a run-time interface can support all the well-known techniques for implementing exceptions, while enabling each individual language to make different decisions about the cost tradeoffs between raising an exception and executing the normal case. A compiler that has a run-time interface, not just the traditional compile-time interface, is significantly easier to reuse with multiple languages.
Again because of the high cost of building a compiler, making it reusable with multiple machines is valuable. To do so, researchers have tried the idea of ``machine description.'' But a typical machine description actually describes an algorithm, not a machine, and does so in terms of a particular compiler's intermediate code, so it can't be reused. The result is that newly developed hardware often has little or no support from such tools as debuggers and profilers, and even basic tools such as assemblers, disassemblers, and emulators are poorly engineered and expensive to produce.
To address these problems, I have pioneered declarative machine descriptions, which say only what the machine does and do so in terms that are independent of particular intermediate codes. Such descriptions are much easier to reuse, and most importantly, they can be reused to help build a wide variety of tools.
In all my work on low-level infrastructure, my results could be characterized by saying that I have shown how apparently ``messy'' problems need not have messy solutions: using principled, rigorous approaches, I have not only solved messy problems but have also identified and distilled out the reusable parts of the solutions. Examples include my work on relocation and register allocation.
Although I have contributed primarily to low-level programming-language infrastructure, I have also made related contributions. Infrastructure is a means to useful programming languages, which in turn are a means to the ultimate goal: the construction of useful programs. To stay in touch with this goal, I have stayed active in—and have contributed to—programming languages and programming technique.
Every compiler is divided into at least two parts: a part that analyzes and validates a program according to the syntax and semantics of the source language, called the front end; and a part that generates code for a target machine, called the back end. These two parts are respectively viewed as high-level and low-level infrastructure. My work has been on back ends, not so much because they are low-level, but because they offer the best prospects for reuse. My thinking is that at the semantic level, different target machines resemble one another much more closely than different source languages, so the prospects of reusing back ends are better.
The biggest part of a back end is the code generator, which consumes a low-level representation of a program and produces efficient code for a target machine. Given a language and machine, building a code generator is a well-understood problem, but one requiring substantial effort—several years or more. It is therefore highly desirable to make one's code generator reusable.
A code generator that can be reused with many machines is called retargetable. Retargetable code generation is a well-studied problem, and solutions are relatively mature. Most solutions involve some sort of program generator—called a ``code-generator generator''—which is driven by a special-purpose language often called a ``machine description.'' I have improved on this technique by introducing declarative machine descriptions.
The goal of reusing a code generator with many languages is an old one. Many attempts, of which the most notorious is UNCOL, have failed. Largely by brute force, a couple of industry groups have achieved short-lived, modest successes for families of similar languages. But nobody has ever succeeded in building a code generator that can support such a range of languages as Ada, C, Cecil, Cedar, Fortran, Haskell, Java, Modula-3, ML and Self. I believe that these failures are rooted in the mistaken notion that a code generator should bridge the gap between source-language features and machine features—in practice, the diversity of language features is too great to be supported by a single interface. My alternative is to identify code-generation technology that is well understood, but expensive to implement, and to develop new ways of encapsulating such technology for reuse. Making a code generator reusable with multiple languages, as well as multiple machines, is the goal of the C-- project, which I lead.
C-- is a joint project with Simon Peyton Jones. We have each had one big idea.
A key trend in the evolution of programming languages is ever-greater reliance on run-time services. To support run-time services, the right approach is to identify a few low-level mechanisms that can be used to implement run-time services in high-level languages: although run-time services are diverse, the set of mechanisms used to implement them is much less so. And a reusable set of mechanisms can reasonably be expected to be useful to implement not only today's run-time services, but the run-time services of the future. The mechanisms I have designed meet a critical criterion for reuse: the author of a front end has the same ability to control cost tradeoffs (policies) that he or she would have with a custom code generator.
Our achievements to date are promising. We have published two design papers: one at PPDP (Principles and Practice of Declarative Programming), on mechanisms for garbage collection (Peyton Jones, Ramsey, and Reig 1999), and one at PLDI, on mechanisms for exceptions (Ramsey and Peyton Jones 2000). A third and final design paper, on ``featherweight'' concurrency, awaits the completion of experimental work. We have also given a 3-hour tutorial at PLDI and a 2-hour tutorial at ICFP.
For six years, my work on C-- has been devoted to building infrastructure. With support from Microsoft and the National Science Foundation, my students and I have created Quick C--, a native-code compiler whose primary goal is to provide a means of evaluating C--'s design, especially the run-time interface. A secondary goal is to provide a vehicle for work on declarative machine descriptions. As is expected of a major effort on infrastructure, work on Quick C-- has also led to some interesting discoveries about implementation, which are discussed below.
My goal for C-- is to change how people think they should implement a new programming language. Current compiler infrastructures deal primarily with the compile-time interface. When it comes to run-time services such as garbage collection or exception handling, a newer infrastructure, such as IBM's Jikes, might provide one implementation; an older infrastructure, such as gcc, typically provides no run-time support. I want builders of compiler infrastructures to recognize that the run-time interface is as important as the compile-time interface, and to provide users of those infrastructures with a means of controlling cost tradeoffs in the run-time system. Ideally, of course, compiler infrastructures will use either the twin C-- interfaces or something very much like them. But if we can simply get people to recognize the need for a run-time interface, even if it doesn't look exactly like ours, I will be satisfied.
Part of the job of a back end is to ensure that separately compiled functions and procedures correctly communicate parameters and results, share machine registers, and share the call stack. This job is done by arranging for such functions and procedures to agree to use registers and the stack in conventional ways; the agreement is called the calling convention. Because the calling convention determines many of the cost tradeoffs involved in function and procedure calls, a reusable back end must give the front end control over details of the calling convention. At the same time, in order to interoperate with existing software, a back end must also support at least one standard calling convention.
The implementation of the calling convention, unlike the rest of the back end, needs to know more than just the semantics of the source language and the target instruction set. Unlike a code generator, the standard calling convention cannot, even in principle, be determined only from the semantics of the two languages; it must be treated as a problem in its own right. At present, calling conventions are described informally. A typical convention is documented in informal English; because English is such a bad tool for the job, it is normally supplemented with pictures. The consequences are that the implementation of the calling convention is hard to get right, and it is responsible for disproportionately many bugs. A more subtle consequence is that it is hard to experiment with different conventions—yet compiler writers have shown repeatedly that custom calling conventions can improve performance dramatically.
To address these problems, my students and I have invested significant effort in understanding procedure calling conventions. Our contribution has been to develop new techniques for specifying and implementing procedure calling conventions. Our techniques not only support standard conventions but also make it easy to create special-purpose, custom conventions. Our most significant result, which appeared at POPL'06 (Olinsky, Lindig, and Ramsey 2006), is that we are the first to give a precise, formal semantics to the specification of parameter passing, which is a major component of calling conventions. Our specifications are also directly executable in a compiler. We have also shown how a simple, declarative language makes it possible to specify precisely and formally the frame-layout information that is normally conveyed informally using pictures (Lindig and Ramsey 2004).
A nice spinoff from Quick C-- is a recent result on using functional languages to write compilers. The result bridges a gap between two different styles of translation. In the functional-language community, the common style of translation is to represent a program as a set of trees, rewrite the trees to other trees, and very late in translation, convert trees to machine instructions. Reasoning about tree rewriting is well understood, and because tree rewriting is well supported in functional languages, it is easy to get these translations right.
In the classic compiler-construction community, by contrast, the common style of translation is to represent a program using control-flow graphs and then to improve the program by mutating those graphs in place. Mutable state makes it much harder to reason about the translations, and it can be very hard to implement some of the recent advances in code improvement, such as the compositional optimizer of Lerner, Grove, and Chambers. With graduate student John Dias, I developed a new representation of control-flow graphs, which although immutable, supports both the classic algorithms based on mutation and also a compositional optimizer. This work was presented at the 2005 ACM SIGPLAN Workshop on ML (Ramsey and Dias 2005).
As noted above, people want software for an increasingly diverse set of machines, including not only PCs but also music players, cell phones, and so on. New machines call for new tools, which today are typically built by hand, at high cost. A long-term goal of my research is instead to generate such tools from simple, concise descriptions of machine properties. The grand challenge is to enable a machine expert to write concise, readable descriptions of the machine's instruction set, and from these descriptions to generate a complete programming environment, that is, all the tools needed to build and run software for that machine. The culmination of this research is still 5 to 10 years off, but the intellectual effort I have invested has already produced a number of results.
The most challenging part of this research program is to generate the compiler, or more precisely, the code generator, from declarative machine descriptions. Machine descriptions have been used to create retargetable code generators, but the descriptions are not reusable. Too often, the organizing principle behind the description is ``everything I need to retarget compiler X.'' Even in the best work, the state of the art in retargetable code generation is mapping: to retarget, write a mapping from intermediate code to target instruction set. But the mapping approach suffers from two serious problems: to write the mapping code requires a dual expert who knows the details of both the intermediate code and the target machine; and because the mapping is tied to this intermediate code, it is impossible to reuse.
The alternative I have developed is the declarative machine description (Ramsey and Fernández 1997; Ramsey and Davidson 1998). Such a description has two distinctive properties:
My work on declarative machine descriptions has been supported by DARPA (through a grant of Jack Davidson's) and by the National Science Foundation. It was recently recognized by an invitation to give the opening talk at the Seventh International Symposium on Practical Aspects of Declarative Languages (PADL 2005). In this work, I have shown that it is helpful to use different description languages for different properties; the two most important properties, which together cover the needs of a wide range of tools, are the binary representation and semantics of instructions.
The binary representation of an instruction set is critically important because it is the only representation that is recognized by the hardware. It is useful not only because it is executable, but because it is the one representation that all programming languages must have in common. As an architecture evolves, its binary representation also evolves, and mature representations—such as the widely used Intel instruction sets—can be very complex. To describe these representations, Mary Fernández and I designed SLED, a Specification Language for Encoding and Decoding (Ramsey and Fernández 1997). We also built the New Jersey Machine-Code Toolkit: this software generates components that manage binary representation, and these components can be used in other tools (Ramsey and Fernández 1995; Ramsey 1996). Many researchers have adopted SLED or the Toolkit. Notable adopters include Cristina Cifuentes of the University of Queensland, who used the Toolkit in her binary translators; Craig Chambers of the University of Washington, who used it in his Vortex compilers; and Neophytos Michael and Andrew Appel, who used SLED in their system for proof-carrying code. SLED was also extended by Jim Larus and Eric Schnarr to create a language for building their Executable Editing Library. Work on SLED has appeared in USENIX, ICSE, TOPLAS, and PLDI.
I developed an interesting analysis that examines a SLED description and derives relocating transformations used in linking. Relocation is the process of resolving references between separately compiled modules; because many references are in the machine instructions themselves, resolving them requires intimate knowledge of the instruction set. Because of the different representations used even within a single instruction set, it is not unusual for there to be one or two dozen ways of resolving an external reference. Before my work, the only way to identify these ways, called relocating transformations, was to have a body of experts study the instruction set and enumerate the relocating transformations by hand. These hand-discovered transformations would then be named and described in a standards document.
This problem seemed to be inherently messy: there was no obvious way to solve it other than by carefully scrutinizing the instruction set and identifying all the cases a linker might have to deal with. But I showed it had a clean, principled solution: I first applied an insight from the λ-calculus to show that resolving a reference is like applying a multiple-argument, curried function. I then developed a new analysis and optimization that, when applied to a SLED specification, discovers the same relocating transformations that are typically found in standards documents (Ramsey 1996). These ideas can greatly simplify the process of developing standards for new instruction sets, and they suggest the possibility of a completely machine-independent linker—one that would be instantly reusable with multiple instruction sets.
The semantics of an instruction set says what each instruction does when executed. I developed a semantic-description language, Lambda-RTL, which is designed to help people write concise, readable descriptions of whole instruction sets in a way that is ``obviously correct'' (Ramsey and Davidson 1998). Lambda-RTL has the potential to solve much harder problems than SLED can, but unlike SLED, it is not easily packaged in a tool that others can use. The difficulty has to do with some important unsolved problems in program generation; my analysis of these problems was published in the Journal of Functional Programming (Ramsey 2003). I have, meanwhile, focused on using Lambda-RTL in my own research, which has led to several new results.
My crispest result, which appeared in ACM TOPLAS (Ramsey and Cifuentes 2003), is a new method for handling delayed-branch instructions in a binary translator or other code analyzer. This problem is repeatedly a stumbling block for industry groups that work with binary codes. But the problem is essential for companies who must migrate legacy code to new hardware; for example, Sun Microsystems has invested in binary-code analysis in order to migrate legacy SPARC codes. Our solution uses Lambda-RTL's semantic framework to derive a translation algorithm that is correct by construction; that is, the correctness of the translation follows from the soundness of each of a series of small program transformations. We also showed the existence of pathological programs that do not have translations and so must be interpreted. The work is coauthored with Cristina Cifuentes, who did the implementation in her UQBT binary translator.
Register allocation, which is to say, the mapping of a program's variables to a machine's registers, is one of the most important problems for compiler writers. Since 1981, compiler writers and researchers have often used Chaitin's classic formulation of the register-allocation problem as a the problem of coloring an interference graph. The difficulty with this formulation is that it assumes all machine registers are indistinguishable, whereas real machines are often irregular: not all registers can be used for all variables. Prior work had addressed this difficulty by various messy, ad hoc means, of which the most common was to attach various ``weights'' to edges of the interference graph. These weights had no clear semantic interpretation; instead, they were algorithmic devices that made allocations come out right most of the time.
My contribution, working with Mike Smith and Glenn Holloway, was to identify a new, clean, principled approach grounded in the machine's semantics. Our approach uses information that can easily be derived from a Lambda-RTL specification: we identify what class of actual machine registers can be used in each instruction, and we identify the pairs of such registers that share state in the hardware. Using this information, I developed an exact colorability criterion for register allocation, and I showed how it could be approximated efficiently. Mike Smith then improved the approximation to account for saturation, i.e., use of all registers in a class. Mike also found a way to update the approximation efficiently in response to incremental changes of an interference graph; incremental update is critical for good compile-time performance. Finally, I showed that for every machine architecture we know of, Mike's method of accounting for saturation produces the best possible approximation.
This work, which we published in PLDI (Smith, Ramsey and Holloway 2004), presents a simple algorithm which is easy to implement, which is clearly related to Chaitin's original algorithm, and whose extensions are clearly grounded in machine properties. We can reasonably hope that it will become the definitive formulation of graph-coloring register allocation.
Much of the best work in retargetable code generation has been done by Jack Davidson and Chris Fraser, either singly or in combination. The gcc compiler, which is the best-known retargetable compiler, is based on Davidson's 1981 doctoral work. With support from the National Science Foundation, my students and I are currently working on ways of automating Davidson's code-generation strategy by using Lambda-RTL and SLED descriptions.
Davidson's strategy uses a three-phase process of code generation. In the first phase, code expansion, a source program is mapped to a sequence of register-transfer lists (RTLs), each of which is semantically equivalent to a single instruction on the target machine. In the second phase, code improvement, register-transfer lists are rewritten to improve performance, while maintaining the equivalence of one register-transfer list to one machine instruction. In the third phase, code emission, the compiler emits the instruction corresponding to each register-transfer list.
Davidson's strategy requires that a compiler have two machine-dependent components: a code expander to map from source code to register-transfer lists, and a recognizer to map from a register-transfer list to a machine instruction. My graduate student John Dias has successfully generated a recognizer from a combination of Lambda-RTL and SLED descriptions; this work appeared in Compiler Construction 2006 (Dias and Ramsey 2006). The code expander is a much greater challenge, but we have some preliminary results on how to restructure a code expander to make it easier to generate.
Unlike a mathematician's arithmetic, a computer's arithmetic is limited in the precision with which it can represent integers. Today's desktop machines typically support either 32-bit or 64-bit arithmetic, but these numbers change as machines evolve. Limited-precision arithmetic presents a new challenge, which arises when we want to reuse a code generator with both multiple machines and multiple source languages: when neither source precision nor target precision can be known in advance, what do we do about a mismatch? The problem of simulating 64-bit arithmetic on 32-bit machines, or more generally multiprecision arithmetic, has been understood for many years, and solutions are available in the form of reusable software libraries. But the problem of simulating 32-bit arithmetic on 64-bit machines, or more generally widening integer arithmetic, had received little attention. With my help, this problem was solved by my graduate student Kevin Redwine (Redwine and Ramsey 2004).
Previous work dealt with only a handful of arithmetic operations; because our solution is informed by declarative machine descriptions, with which it shares a semantic framework, our solution is comprehensive. The most interesting contribution is not the algorithm itself, but a simple type system which classifies all arithmetic operations according to how they may be handled using a machine word that is too wide. This classification not only assists the algorithm but also identifies exactly the operations that cannot be widened and so must be simulated in software.
Source-level debuggers, when provided at all, tend to be limited in capability and not well liked. As a graduate student, I thought I saw an opportunity there, but I discovered that not enough was known about building debuggers, so as my dissertation project I built a retargetable debugger, ldb (Ramsey and Hanson 1992; Ramsey 1994). My contribution was to show that by getting modest help from the compiler, I could reduce retargeting cost by a factor of five as compared with the most popular Unix debugger, gdb.
Much later, working at Harvard with postdoctoral associate Sukyoung Ryu, I investigated how to reuse a debugger with multiple languages, and in particular, how to do so at minimum cost to the people writing the compilers for those languages. Our contribution was to develop new techniques for supporting a debugger while reusing an existing compiler's code. These techniques, which are embodied in a reusable compile-time support library, rely on four new principles:
I participated in the early phases of the University of Queensland
Binary Translation project headed by Cristina Cifuentes.
We started with two goals:
to develop a binary translator that could be reused with multiple
machines
and
to develop new optimizations for binary translation.
My primary contribution was the algorithm for handling delayed branches
discussed above, but I also made
significant contributions to the design of the translator, which was
published in the Working Conference on Reverse Engineering.
I also co-wrote the proposal which got the initial funding from the
Australian Research Council.
Interpreters, reusable and otherwise
Most of my work addresses what happens at the interface between a language's implementation and a target machine, but I have also worked on interpreters, which provide a way to implement a programming language while letting some other software deal with the target machine. In teaching, I use interpreters to help students learn to work with new programming languages and to understand new programming-language features. In research, we use an embedded interpreter to configure our Quick C-- compiler; the embedded interpreter gives us a number of advantages in testing, distributing, and debugging the compiler. Interpreters are well understood, but I have discovered that writing interpreters in functional languages enables new techniques that are not available in imperative languages.
The purpose of an embedded interpreter is to provide a scripting capability to applications, such as the Quick C-- compiler, written in a host language. A critical goal is to write the interpreter once and to reuse it to control many different applications. To enable the embedded interpreter to control an application, it must be possible to embed host-language application values into the interpreted language, and dually to project embedded values back to the host language. In the previous state of the art, embedding and projection could be achieved only by a special-purpose glue function, normally written by hand, for each underlying host function used by the interpreter. My contribution was to show how glue functions could be eliminated; using my technique, we embed and project each host function by means of a simple, declarative description of the function's type. This solution is especially satisfying because programmers using functional languages already think in terms of such types. The work was first published in a workshop (Ramsey 2003), and a revised, extended version has been accepted for publication in the Journal of Functional Programming.
The value of an embedded interpreter is significantly enhanced if the interpreter can represent host values that have types other than the ones built into the interpreter. Standard practice has been to enable a programmer to add new types of values as extensions, but in previous work, such extensions are unsafe. This means that each extension relies on the programmer to identify its new type accurately, and if the programmer makes a mistake, the program can fail in unpredictable ways. Previous work in functional languages showed how to build an extensible interpreter safely, but only in a way that prevented the interpreter from being compiled separately from the host application—and therefore also prevented it from being easily reused. My contribution has been to show that by clever use of the ML modules system, it is possible to build an extensible interpreter that simultaneously provides both type safety and separate compilation (Ramsey 2005).
My work on the implementations of SLED and Lambda-RTL led to a couple of results that cover other aspects of programming-language infrastructure. The first result bears on program generation, which is a technique that I, along with many others, have used repeatedly. To make it easier to debug a program generator, and to help convince prospective users that the generator can be trusted, the generated code should be as idiomatic and readable as possible. My contribution was to show how to generate code that improves readability by using infix, prefix, and postfix operators, without unnecessary parentheses (Ramsey 1998).
The second result is about error messages. When a program contains an error, a compiler may make assumptions that lead to further, spurious error messages, which can overwhelm the programmer. Earlier researchers had shown how to reduce or eliminate spurious error messages about bad syntax, by using so-called error-correcting parsers. My contribution was to show how to eliminate spurious error messages about bad static semantics. I did so by means of a programming discipline that uses the error monad of Spivey (1990) and Wadler (1992) to account for intermediate results that are unavailable because of a previously detected error. My discipline prevents an unavailable result from leading to a new error message, and even better, it uses the ML type system to identify exactly those places in the compiler where a result is potentially unavailable and must be accounted for (Ramsey 1999).
In addition to work on programming-language infrastructure, I have done other work in the broader area of languages and tools. Here I summarize two language-design results as well as work in support of file synchronization and literate programming. I have omitted early work in formal methods.
Although the ML modules system is the most powerful system known, it is weak when it comes to specifying interfaces. For about ten years, I have wanted to improve this situation, and with Kathleen Fisher and my student Paul Govereau, I developed a proposal, which has been published in ICFP (Ramsey, Fisher, and Govereau 2005). The key idea behind the proposal is to provide the same expressive power in the signature language that we expect from libraries that manipulate sets and finite maps.
Language-design work is always tricky to evaluate, since it is hard to predict what ideas might be adopted, or even just influential. And modules are an especially difficult part of language design; exciting results are rare. With those caveats, I am optimistic about this work; it is solidly grounded both practically and theoretically, and it improves a major functional language.
A language is probabilistic if it can model events that are not certain to occur but occur only with some probability. Efficient reasoning about probabilistic models is an area in which my Harvard colleague Avi Pfeffer is a distinguished scholar, and Avi has found ways to embody such reasoning in a high-level programming language. Avi describes his language in terms of the algorithms and data structures needed to reason efficiently, and I wanted to understand how these algorithms and data structures relate to probability. The result was a joint paper, which proves that probability distributions form a monad, shows that Avi's view is equivalent to the monadic view, and explains why Avi's view results in more efficient reasoning (Ramsey and Pfeffer 2002). This work is only an initial step; many interesting foundational questions are left open.
File synchronization is the problem of restoring consistency after users have made changes to different replicas of a file system. This problem is far afield from programming languages, but fellow languages researcher Benjamin Pierce got me interested around 1999. After reading Pierce's paper with Balasubramaniam (1998), I became convinced I had a better approach. With a visiting high-school student, Elod Csirmaz, I developed the approach and proved it at least as strong as Balasubramaniam and Pierce's approach; we published our results in Foundations of Software Engineering (Ramsey and Csirmaz 2001).
Literate programming is a programming discipline that Don Knuth invented to help make programs easier for people to understand, extend, and modify. My work on literate programming was finished long ago, but it has been influential. I built the first literate-programming tools to be reusable with multiple languages, and my language-independent literate-programming tool, noweb (Ramsey 1994), has not only become the dominant tool but has also influenced other tools. There is nothing deep about noweb, but it is carefully engineered to have just the right combination of simplicity and extensibility. Knuth himself adopted one of noweb's ideas in revising CWEB, his preferred literate-programming tool.
Literate programming has been a significant influence on tools like Perl's POD and Java's Javadoc, which are very widely used. Although literate programming as envisioned by Knuth is practiced largely by mathematicians, statisticians, and physicists, there is a significant cadre of computer scientists using the technique, and noweb has been very influential among this group.