Another DSL for pictures? Seems fishy. But hold fast as we chart a course to an embedded DSL for the domain of slide presentations with animations. Our DSL programs interact with the host language in two ways: by allowing pictures and animations to be built using host-language functions (resembling a shallow embedding), and by allowing host-language reflection on their construction (resembling a deep embedding). As a result, users can define their own animation combinators but still also inspect, adjust, and reassemble animations. To demonstrate our DSL's expressive power, we show how it supports a Keynote-like Magic Move operation. Having made the DSL shipshape, we dive into a lesson learned about deep and shallow DSL design. While deep and shallow may seem like mutually exclusive options, we argue they are actually points on an entire spectrum of possible DSL designs. More importantly, our paper demonstrates that points on the spectrum between deep and shallow are where DSL designs achieve full sail.

Over the last 15 years, researchers have studied a wide variety of important aspects of contract systems, ranging from internal consistency (complete monitoring and correct blame) to subtle details about the semantics of contracts combinators (dependency) to the difficulty of efficient checking (avoiding asymptotically bad redundant checking). Although each paper offers essential insights about contract systems, they also differ in inessential ways, making it hard to know how their metatheories combine. Even worse, the metatheories share tremendous tedium in their definitions and proofs, occupying researchers’ time with no benefit. In this paper, we present the idea that higher-order contract systems can be viewed as transition systems and show that this perspective offers an important opportunity for reuse in their metatheories. We demonstrate the value of this perspective by proving representative properties from the literature, and by contributing a new proof establishing that elimination of redundant contract checks can eliminate asymptotic slowdowns. To confirm our claims and encourage the adoption of our ideas, we provide a mechanized development in Agda.

Conventional wisdom suggests that the benefits of functional programming no longer apply in the presence of even a small amount of imperative code, as if the addition of imperative code effectively subtracts. And yet, as we show in this paper, combining functional programming with the special imperative language Esterel provides a multiplicative improvement to the benefits of functional programming. The key to the benefit of both Esterel and functional programming stems from a restriction that both share. As in functional programming, where only the inputs to a function determine its outputs, the state of an Esterel computation is fully determined by the program’s input and the state that the computation had in the previous time step, where the notion of a time step is explicit in the language. Esterel’s guarantee holds even though Esterel programs feature concurrent threads, mutable state, and the ability to create, suspend, and even terminate threads as the computation proceeds. This similarity is the root of the benefits that programmers accrue as they informally reason about their program’s behavior. To illustrate these benefits, the bulk of this paper consists of an in-depth exploration of HipHop code (a mashup of JavaScript and Esterel) that implements a Sudoku solver, showing how it is possible to write code that is as easy to understand as if it were written in a pure functional programming style, even though it uses multiple threads, mutable state, thread preemption, and even thread abortion. Even better, concurrent composition and task canceling provide significant program structuring benefits that allow a clean decomposition and task separation in the solver.

Rhombus is a new language that is built on Racket. It offers the same kind of language extensibility as Racket itself, but using traditional (infix) notation. Although Rhombus is far from the first language to support Lisp-style macros without Lisp-style parentheses, Rhombus offers a novel synthesis of macro technology that is practical and expressive. A key element is the use of multiple binding spaces for context-specific sublanguages. For example, expressions and pattern-matching forms can use the same operators with different meanings and without creating conflicts. Context-sensitive bindings, in turn, facilitate a language design that reduces the notational distance between the core language and macro facilities. For example, repetitions can be defined and used in binding and expression contexts generally, which enables a smoother transition from programming to metaprogramming. Finally, since handling static information (such as types) is also a necessary part of growing macros beyond Lisp, Rhombus includes support in its expansion protocol for communicating static information among bindings and expressions. The Rhombus implementation demonstrates that all of these pieces can work together in a coherent and user-friendly language.

The DefinitelyTyped repository hosts type declarations for thousands of JavaScript libraries. Given the lack of formal connection between the types and the corresponding code, a natural question is are the types right? An equally important question, as DefinitelyTyped and the libraries it supports change over time, is how can we keep the types from becoming wrong? In this paper we offer Scotty, a tool that detects mismatches between the types and code in the Definitely-Typed repository. More specifically, Scotty checks each package by converting its types into contracts and installing the contracts on the boundary between the library and its test suite. Running the test suite in this environment can reveal mismatches between the types and the JavaScript code. As automation and generality are both essential if such a tool is going to remain useful in the long term, we focus on techniques that sacrifice completeness, instead preferring to avoid false positives. Scotty currently handles about 26% of the 8006 packages on DefinitelyTyped (61% of the packages whose code is available and whose test suite passes). Perhaps unsurprisingly, running the tests with these contracts in place revealed many errors in Definitely-Typed. More surprisingly, despite the inherent limitations of the techniques we use, this exercise led to one hundred accepted pull requests that fix errors in DefinitelyTyped, demonstrating the value of this approach for the long-term maintenance of DefinitelyTyped. It also revealed a number of lessons about working in the JavaScript ecosystem and how details beyond the semantics of the language can be surprisingly important. Best of all, it also revealed a few places where programmers preferred incorrect types, suggesting some avenues of research to improve TypeScript.

Abstract Higher-order functions have become a staple of modern programming languages. However, such values stymie concolic testers, as the SMT solvers at their hearts are inherently first-order. This paper lays a formal foundations for concolic testing higher-order functional programs. Three ideas enable our results: (i) our tester considers only program inputs in a canonical form; (ii) it collects novel constraints from the evaluation of the canonical inputs to search the space of inputs with partial help from an SMT solver and (iii) it collects constraints from canonical inputs even when they are arguments to concretized calls. We prove that (i) concolic evaluation is sound with respect to concrete evaluation; (ii) modulo concretization and SMT solver incompleteness, the search for a counter-example succeeds if a user program has a bug and (iii) this search amounts to directed evolution of inputs targeting hard-to-reach corners of the program.

Inline caches and hidden classes are two essential components for closing the performance gap between static languages such as Java, Scheme, or ML and dynamic languages such as JavaScript or Python. They rely on the observation that for a particular object access located at a particular point of the program, the shapes, usually referred to as the hidden classes, of accessed objects are likely to be the same. Taking benefit of that invariant, they replace the expensive lookup the semantics of these languages normally demand with one test, the inline cache, and a memory read indexed by an offset computed during the last cache miss. These optimizations are essential but they are not general enough to cope with JavaScript’s proxies. In particular, when the property name is itself unknown statically, inline cache-based optimizations always take a slow path.

Contract systems, especially of the higher-order flavor, go hand in hand with blame. The pragmatic purpose of blame is to narrow down the code that a programmer needs to examine to locate the bug when the contract system discovers a contract violation. Or so the literature on higher-order contracts claims. In reality, however, there is neither empirical nor theoretical evidence that connects blame with the location of bugs. The reputation of blame as a tool for weeding out bugs rests on anecdotes about how programmers use contracts to shift blame and their attention from one part of a program to another until they discover the source of the problem. This paper aims to fill the apparent gap and shed light to the relation between blame and bugs. To that end, we introduce an empirical methodology for investigating whether, for a given contract system, it is possible to translate blame information to the location of bugs in a systematic manner. Our methodology is inspired by how programmers attempt to increase the precision of the contracts of a blamed component in order to shift blame to another component, which becomes the next candidate for containing the bug. In particular, we construct a framework that enables us to ask for a contract system whether (i) the process of blame shifting causes blame to eventually settle to the component that contains the bug; and (ii) every shift moves blame ``closer'' to the faulty component. Our methodology offers a rigorous means for evaluating the pragmatics of contract systems, and we employ it to analyze Racket's contract system. Along the way, we uncover subtle points about the pragmatic meaning of contracts and blame in Racket: (i) the expressiveness of Racket's off-the-shelf contract language is not sufficient to narrow down the blamed portion of the code to the faulty component in all cases; and (ii) contracts that trigger state changes (even unexpectedly, perhaps in the runtime system's data structures or caches) interfere with program evaluation in subtle ways and thus blame shifting can lead programmers on a detour when searching for a bug. These points highlight how evaluations such as ours suggest fixes to language design.

Abstract A sound gradual type system ensures that untyped components of a program can never break the guarantees of statically typed components. This assurance relies on runtime checks, which in turn impose performance overhead in proportion to the frequency and nature of interaction between typed and untyped components. The literature on gradual typing lacks rigorous descriptions of methods for measuring the performance of gradual type systems. This gap has consequences for the implementors of gradual type systems and developers who use such systems. Without systematic evaluation of mixed-typed programs, implementors cannot precisely determine how improvements to a gradual type system affect performance. Developers cannot predict whether adding types to part of a program will significantly degrade (or improve) its performance. This paper presents the first method for evaluating the performance of sound gradual type systems. The method quantifies both the absolute performance of a gradual type system and the relative performance of two implementations of the same gradual type system. To validate the method, the paper reports on its application to 20 programs and 3 implementations of Typed Racket.

The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs. Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically. This paper presents the first such equational calculus for Esterel. It also illustrates the calculus’s usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.

The promise of gradual typing is that programmers should get the best of both worlds: the static guarantees of static types, and the dynamic flexibility of untyped programming. This is an enticing benefit, but one that, in practice, may carry significant costs. Significant enough, in fact, to threaten the very practicality of gradual typing; slowdowns as high as 120x are reported as arising from gradual typing. If one examines these results closely, though, it becomes clear that the costs of gradual typing are not evenly distributed. Indeed, while mixing typed and untyped code almost invariably carries non-trivial costs, many truly deal-breaking slowdowns exhibit pathological performance. Unfortunately, the very presence of these pathological cases---and therefore the possibility of hitting them during development---makes gradual typing a risky proposition in any setting that even remotely cares about performance. This work attacks one source of large overheads in these pathological cases: an accumulation of contract wrappers that perform redundant checks. The work introduces a novel strategy for contract checking---collapsible contracts---which eliminates this redundancy for function and vector contracts and drastically reduces the overhead of contract wrappers. We implemented this checking strategy as part of the Racket contract system, which is used in the Typed Racket gradual typing system. Our experiments show that our strategy successfully brings a class of pathological cases in line with normal cases, while not introducing an undue overhead to any of the other cases. Our results also show that the performance of gradual typing in Racket remains prohibitive for many programs, but that collapsible contracts are one essential ingredient in reducing the cost of gradual typing.

A medical prescription is a set of health care instructions that govern the plan of care for an individual patient, which may include orders for drug therapy, diet, clinical assessment, and laboratory testing. Clinicians have long used algorithmic thinking to describe and implement prescriptions but without the benefit of a formal programming language. Instead, medical algorithms are expressed using a natural language patois, flowcharts, or as structured data in an electronic medical record system. The lack of a prescription programming language inhibits expressiveness; results in prescriptions that are difficult to understand, hard to debug, and awkward to reuse; and increases the risk of fatal medical error. This article reports on the design and evaluation of Patient-Oriented Prescription Programming Language (POP-PL), a domain-specific programming language designed for expressing prescriptions. The language is based around the idea that programs and humans have complementary strengths that, when combined properly, can make for safer, more accurate performance of prescriptions. Use of POP-PL facilitates automation of certain low-level vigilance tasks, freeing up human cognition for abstract thinking, compassion, and human communication. We implemented this language and evaluated its design attempting to write prescriptions in the new language and evaluated its usability by assessing whether clinicians can understand and modify prescriptions written in the language. We found that some medical prescriptions can be expressed in a formal domain-specific programming language, and we determined that medical professionals can understand and correctly modify programs written in POP-PL. We also discuss opportunities for refining and further developing POP-PL.

Abstract Enumerations represented as bijections between the natural numbers and elements of some given type have recently garnered interest in property-based testing because of their efficiency and flexibility. There are, however, many ways of defining these bijections, some of which are better than others. This paper offers a new property of enumeration combinators called fairness that identifies enumeration combinators that are better suited to property-based testing. Intuitively, the result of a fair combinator indexes into its argument enumerations equally when constructing its result. For example, extracting the n th element from our enumeration of three-tuples indexes about $\sqrt[3]{n}$ elements into each of its components instead of, say, indexing $\sqrt[2]{n}$ into one and $\sqrt[4]{n}$ into the other two, as you would if a three-tuple were built out of nested pairs. Similarly, extracting the n th element from our enumeration of a three-way union returns an element that is $\frac{n}{3}$ into one of the argument enumerators. The paper presents a semantics of enumeration combinators, a theory of fairness, proofs establishing fairness of our new combinators and that some combinations of fair combinators are not fair. We also report on an evaluation of fairness for the purpose of finding bugs in programming-language models. We show that fair enumeration combinators have complementary strengths to an existing, well-tuned ad hoc random generator (better on short time scales and worse on long time scales) and that using unfair combinators is worse across the board.

Domain-specific languages are the ultimate abstraction, dixit Paul Hudak. But what abstraction should we use to build such ultimate abstractions? What is sauce for the goose is sauce for the gander: a language, of course! Racket is the ultimate abstraction-abstraction, a platform for quickly and easily building new ultimate abstractions. This pearl demonstrates Racket's power by taking a leisurely walk through the implementation of a DSL for Lindenmayer systems, the computational model par excellence of theoretical botany.

Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, completely forgetting about their pragmatics.

Existing programming language access control frameworks do not meet the needs of all software components. We propose an expressive framework for implementing access control monitors for components. The basis of the framework is a novel concept: the authority environment. An authority environment associates rights with an execution context. The building blocks of access control monitors in our framework are authorization contracts: software contracts that manage authority environments. We demonstrate the expressiveness of our framework by implementing a diverse set of existing access control mechanisms and writing custom access control monitors for three realistic case studies.

Over the past 20 years, programmers have embraced dynamically-typed programming languages. By now, they have also come to realize that programs in these languages lack reliable type information for software engineering purposes. Gradual typing addresses this problem; it empowers programmers to annotate an existing system with sound type information on a piecemeal basis. This paper presents an implementation of a gradual type system for a full-featured class-based language as well as a novel performance evaluation framework for gradual typing.

Medical professionals have long used algorithmic thinking to describe and implement health care processes without the benefit of the conceptual framework provided by a programming language. Instead, medical algorithms are expressed using English, flowcharts, or data tables. This results in prescriptions that are difficult to understand, hard to debug, and awkward to reuse. This paper reports on the design and evaluation of a domain-specific programming language, POP-PL for expressing medical algorithms. The design draws on the experience of researchers in two disciplines, programming languages and medicine. The language is based around the idea that programs and humans have complementary strengths, that when combined can make for safer, more accurate performance of prescriptions. We implemented a prototype of our language and evaluated its design by writing prescriptions in the new language and administering a usability survey to medical professionals. This formative evaluation suggests that medical prescriptions can be conveyed by a programming language's mode of expression and provides useful information for refining the language. Analysis of the survey results suggests that medical professionals can understand and correctly modify programs in POP-PL.

Programmers embrace contracts. They can use the language they know and love to formulate logical assertions about the behavior of their programs. They can use the existing IDE infrastructure to log contracts, to test, to debug, and to profile their programs.

The 17th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 10–12, 2012 in Copenhagen, Denmark. After the conference, the programme committee selected several outstanding papers and invited their authors to submit to this special issue of Journal of Functional Programming . Robby Findler and Satnam Singh acted as editors for these submissions. This issue includes the accepted papers, each of which provides substantial new material beyond the original conference version.

Many languages support behavioral software contracts so that programmers can describe a component's obligations and promises via logical assertions in its interface. The contract system monitors program execution, checks whether the assertions hold, and, if not, blames the guilty component. Pinning down the violator gets the debugging process started in the right direction. Quality contracts impose a serious run-time cost, however, and programmers therefore compromise in many ways. Some turn off contracts for deployment, but then contracts and code quickly get out of sync during maintenance. Others test contracts randomly or probabilistically. In all cases, programmers have to cope with lack of blame information when the program eventually fails.

Given the widespread use of memory-safe languages, students must understand garbage collection well. Following a constructivist philosophy, an effective approach would be to have them implement garbage collectors. Unfortunately, a full implementation depends on substantial knowledge of compilers and runtime systems, which many courses do not cover or cannot assume.

Chaperones and impersonators provide run-time support for interposing on primitive operations such as function calls, array access and update, and structure field access and update. Unlike most interposition support, chaperones and impersonators are restricted so that they constrain the behavior of the interposing code to reasonable interposition, which in practice preserves the abstraction mechanisms and reasoning that programmers and compiler analyses rely on.

Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language tool; or the essence of a program analysis. No matter which role it plays, however, a faulty model doesn't serve its purpose.

Abstract Racket is a large language that is built mostly within itself. Unlike the usual approach taken by non-Lisp languages, the self-hosting of Racket is not a matter of bootstrapping one implementation through a previous implementation, but instead a matter of building a tower of languages and libraries via macros. The upper layers of the tower include a class system, a component system, pedagogic variants of Scheme, a statically typed dialect of Scheme, and more. The demands of this language-construction effort require a macro system that is substantially more expressive than previous macro systems. In particular, while conventional Scheme macro systems handle stand-alone syntactic forms adequately, they provide weak support for macros that share information or macros that use existing syntactic forms in new contexts. This paper describes and models features of the Racket macro system, including support for general compile-time bindings, sub-form expansion and analysis, and environment management. The presentation assumes a basic familiarity with Lisp-style macros, and it takes for granted the need for macros that respect lexical scope. The model, however, strips away the pattern and template system that is normally associated with Scheme macros, isolating a core that is simpler, can support pattern and template forms themselves as macros, and generalizes naturally to Racket's other extensions.

By adjusting the design of the ISA and enabling circuit timing-sensitive optimizations in a compiler, we can more effectively exploit timing speculation. While there has been growing interest in systems that leverage circuit-level timing speculation to improve the performance and power-efficiency of processors, most of the innovation has been at the microarchitectural level. We make the observation that some code sequences place greater demand on circuit timing deadlines than others. Furthermore, by selectively replacing these codes with instruction sequences which are semantically equivalent but reduce activity on timing critical circuit paths, we can trigger fewer timing errors and hence reduce recovery costs.

Places bring new support for message-passing parallelism to Racket. This paper gives an overview of the programming model and how we had to modify our existing, sequential runtime-system to support places. We show that the freedom to design the programming model helped us to make the implementation tractable; specifically, we avoided the conventional pain of adding just the right amount of locking to a big, legacy runtime system. The paper presents an evaluation of the design that includes both a real-world application and standard parallel benchmarks.

Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0 and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, Eugster, Field, Nystrom, and Vitek, 2009). However, an important open question remains, which is how to add parametric polymorphism to languages that combine static and dynamic typing. We present a system that permits a value of dynamic type to be cast to a polymorphic type and vice versa, with relational parametricity enforced by a kind of dynamic sealing along the lines proposed by Matthews and Ahmed (2008) and Neis, Dreyer, and Rossberg (2009). Our system includes a notion of blame, which allows us to show that when casting between a more-precise type and a less-precise type, any cast failures are due to the less-precisely-typed portion of the program. We also show that a cast from a subtype to its supertype cannot fail.

Behavioral software contracts supplement interface information with logical assertions. A rigorous enforcement of contracts provides useful feedback to developers if it signals contract violations as soon as they occur and if it assigns blame to violators with preciseexplanations. Correct blame assignment gets programmers started with the debugging process and can significantly decrease the time needed to discover and fix bugs.

Testing is among the most effective tools available for finding bugs. Still, we know of no automatic technique for generating test cases that expose bugs involving a combination of mutable state and callbacks, even though objects and method overriding set up exactly that combination. For such cases, a test generator must create callbacks or subclasses that aggressively exercise side-effecting operations using combinations of generated objects.This paper presents a new algorithm for randomly testing programs that use state and callbacks. Our algorithm exploits a combination of contracts and environment bindings to guide the test-case generator toward interesting inputs. Our prototype implementation for Racket (formerly PLT Scheme) - which has a Java-like class system, but with first-class classes as well as gbeta-like augmentable methods - uncovered dozens of bugs in a well-tested and widely used text-editor library.We describe our approach in a precise, formal notation, borrowing the techniques used to describe operational semantics and type systems. The formalism enables us to provide a compact and self-contained explanation of the core of our technique without the ambiguity usually present in pseudo-code descriptions.

Many language implementations, particularly for high-level and scripting languages, are based on carefully honed runtime systems that have an internally sequential execution model. Adding support for parallelism in the usual form -- as threads that run arbitrary code in parallel -- would require a major revision or even a rewrite to add safe and efficient locking and communication. We describe an alternative approach to incremental parallelization of runtime systems. This approach can be applied inexpensively to many sequential runtime systems, and we demonstrate its effectiveness in the Racket runtime system and Parrot virtual machine. Our evaluation assesses both the performance benefits and the developer effort needed to implement our approach. We find that incremental parallelization can provide useful, scalable parallelism on commodity multicore processors at a fraction of the effort required to implement conventional parallel threads.

Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics courses would make pre-algebra course come alive. If input and output were invisible, students could implement fun simulations, animations, and even interactive and distributed games all while using nothing more than plain mathematics. We have implemented this vision with a simple framework for purely functional I/O. Using this framework, students design, implement, and test plain mathematical functions over numbers, booleans, string, and images. Then the framework wires them up to devices and performs all the translation from external information to internal data (and vice versa)--just like every other operating system. Once middle school students are hooked on this form of programming, our curriculum provides a smooth path for them from pre-algebra to freshman courses in college on object-oriented design and theorem proving.

Scribble is a system for writing library documentation, user guides, and tutorials. It builds on PLT Scheme's technology for language extension, and at its heart is a new approach to connecting prose references with library bindings. Besides the base system, we have built Scribble libraries for JavaDoc-style API documentation, literate programming, and conference papers. We have used Scribble to produce thousands of pages of documentation for PLT Scheme; the new documentation is more complete, more accessible, and better organized, thanks in large part to Scribble's flexibility and the ease with which we cross-reference information across levels. This paper reports on the use of Scribble and on its design as both an extension and an extensible part of PLT Scheme.

Interoperability is big business, a fact to which .NET, the JVM, and COM can attest. Language designers are well aware of this, and they are designing programming languages that reflect it—for instance, SML.NET, F#, Mondrian, and Scala all treat interoperability as a central design feature. Still, current multi-language research tends not to focus on the semantics of these features, but only on how to implement them efficiently. In this article, we attempt to rectify that by giving a technique for specifying the operational semantics of a multi-language system as a composition of the models of its constituent languages. Our technique abstracts away the low-level details of interoperability like garbage collection and representation coherence, and lets us focus on semantic properties like type-safety, equivalence, and termination behavior. In doing so it allows us to adapt standard theoretical techniques such as subject-reduction, logical relations, and operational equivalence for use on multi-language systems. Generally speaking, our proofs of properties in a multi-language context are mutually referential versions of their single language counterparts. We demonstrate our technique with a series of strategies for embedding a Scheme-like language into an ML-like language. We start by connecting very simple languages with a very simple strategy, and work our way up to languages that interact in sophisticated ways and have sophisticated features such as polymorphism and effects. Along the way, we prove relevant results such as type-soundness and termination for each system we present using adaptations of standard techniques. Beyond giving simple expressive models, our studies have uncovered several interesting facts about interoperability. For example, higher-order function contracts naturally emerge as the glue to ensure that interoperating languages respect each other's type systems. Our models also predict that the embedding strategy where foreign values are opaque is as expressive as the embedding strategy where foreign values are translated to corresponding values in the other language, and we were able to experimentally verify this behavior using PLT Scheme's foreign function interface.

Abstract This paper presents an operational semantics for the core of Scheme. Our specification improves over the denotational semantics from the Revised 5 Report on Scheme specification in four ways. First, it covers a larger part of the language, specifically eval , quote , dynamic-wind , and the top level. Second, it models multiple values in a way that does not require changes to unrelated parts of the language. Third, it provides a faithful model of Scheme's undefined order of evaluation. Finally, we have implemented our specification in PLT Redex, a domain-specific language for writing operational semantics. The implementation allows others to experiment with our specification and allows us to build a specification test suite, which improves our confidence that our system is a faithful model of Scheme. In addition to a specification of Scheme, this paper contributes three novel modeling techniques for Felleisen Hieb-style rewriting semantics. All three techniques are applicable to a wider range of problems than modeling Scheme, and they combine seamlessly in our model, suggesting that they would scale to complete models of other languages.

The analogy between types and contracts raises the question of how many features of static type systems can be expressed as dynamic contracts. An important feature missing in prior work on contracts is parametricity, as represented by the polymorphic types in languages like Standard ML.

Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programming language research. Numerous papers explain their advantages, how the operators explain each other (or don't), and other aspects of the operators' existence. Production programming languages, however, do not support these operators, partly because their relationship to existing and demonstrably useful constructs - such as exceptions and dynamic binding - remains relatively unexplored.

Inter-language interoperability is big business, as the success of Microsoft's .NET and COM and Sun's JVM show. Programming language designers are designing programming languages that reflect that fact --- SML#, Mondrian, and Scala, to name just a few examples, all treat interoperability with other languages as a central design feature. Still, current multi-language research tends not to focus on the semantics of interoperation features, but only on how to implement them efficiently. In this paper, we take first steps toward higher-level models of interoperating systems. Our technique abstracts away the low-level details of interoperability like garbage collection and representation coherence, and lets us focus on semantic properties like type-safety and observable equivalence.Beyond giving simple expressive models that are natural compositions of single-language models, our studies have uncovered several interesting facts about interoperability. For example, higher-order contracts naturally emerge as the glue to ensure that interoperating languages respect each other's type systems. While we present our results in an abstract setting, they shed light on real multi-language systems and tools such as the JNI, SWIG, and Haskell's stable pointers.

In PLT Scheme, programs consist of modules with contracts. The latter describe the inputs and outputs of functions and objects via predicates. A run-time system enforces these predicates; if a predicate fails, the enforcer raises an exception that blames a specific module with an explanation of the fault.In this paper, we show how to use such module contracts to turn set-based analysis into a fully modular parameterized analysis. Using this analysis, a static debugger can indicate for any given contract check whether the corresponding predicate is always satisfied, partially satisfied, or (potentially) completely violated. The static debugger can also predict the source of potential errors, i.e., it is sound with respect to the blame assignment of the contract system.

Among systems for creating slide presentations, the dominant ones offer essentially no abstraction capability. Slideshow represents our effort over the last several years to build an abstraction-friendly slide system with PLT Scheme. We show how functional programming is well suited to the task of slide creation, we report on the programming contructs that we have developed for slides, and we describe our solutions to practical problems in rendering slides. We also describe experimental extensions to DrScheme that support a mixture of programmatic and WYSIWYG slide creation.

As a value flows across the boundary between interoperating languages, it must be checked and converted to fit the types and representations of the target language. For simple forms of data, the checks and coercions can be immediate; for higher order data, such as functions and objects, some must be delayed until the value is used in a particular way. Typically, these coercions and checks are implemented by an ad-hoc mixture of wrappers, reflection, and dynamic predicates. We observe that 1) the wrapper and reflection operations fit the profile of mirrors, 2) the checks correspond to contracts, and 3) the timing and shape of mirror operations coincide with the timing and shape of contract operations. Based on these insights, we present a new model of interoperability that builds on the ideas of mirrors and contracts, and we describe an interoperable implementation of Java and Scheme that is guided by the model.

In an object-oriented language, a derived class may declare a method with the same signature as a method in the base class. The meaning of the re-declaration depends on the language. Most commonly, the new declaration overrides the base declaration, perhaps completely replacing it, or perhaps using super to invoke the old implementation. Another possibility is that the base class always controls the method implementation, and the new declaration merely augments the method in the case that the base method calls inner. Each possibility has advantages and disadvantages. In this paper, we explain why programmers need both kinds of method redeclaration, and we present a language that integrates them. We also present a formal semantics for the new language, and we describe an implementation for MzScheme.

When an individual task can be forcefully terminated at any time, cooperating tasks must communicate carefully. For example, if two tasks share an object, and if one task is terminated while it manipulates the object, the object may remain in an inconsistent or frozen state that incapacitates the other task. To support communication among terminable tasks, language run-time systems (and operating systems) provide kill-safe abstractions for inter-task communication. No kill-safe guarantee is available, however, for abstractions that are implemented outside the run-time system.In this paper, we show how a run-time system can support new kill-safe abstractions without requiring modification to the run-time system, and without requiring the run-time system to trust any new code. Our design frees the run-time implementor to provide only a modest set of synchronization primitives in the trusted computing base, while still allowing tasks to communicate using sophisticated abstractions.

Twenty years ago Abelson and Sussman's Structure and Interpretation of Computer Programs radically changed the intellectual landscape of introductory computing courses. Instead of teaching some currently fashionable programming language, it employed Scheme and functional programming to teach important ideas. Introductory courses based on the book showed up around the world and made Scheme and functional programming popular. Unfortunately, these courses quickly disappeared again due to shortcomings of the book and the whimsies of Scheme. Worse, the experiment left people with a bad impression of Scheme and functional programming in general. In this pearl, we propose an alternative role for functional programming in the first-year curriculum. Specifically, we present a framework for discussing the first-year curriculum and, based on it, the design rationale for our book and course, dubbed How to Design Programs . The approach emphasizes the systematic design of programs. Experience shows that it works extremely well as a preparation for a course on object-oriented programming.

Assertions play an important role in the construction of robust software. Their use in programming languages dates back to the 1970s. Eiffel, an object-oriented programming language, wholeheartedly adopted assertions and developed the "Design by Contract" philosophy. Indeed, the entire object-oriented community recognizes the value of assertion-based contracts on methods.In contrast, languages with higher-order functions do not support assertion-based contracts. Because predicates on functions are, in general, undecidable, specifying such predicates appears to be meaningless. Instead, the functional languages community developed type systems that statically approximate interesting predicates.In this paper, we show how to support higher-order function contracts in a theoretically well-founded and practically viable manner. Specifically, we introduce λcon, a typed lambda calculus with assertions for higher-order functions. The calculus models the assertion monitoring system that we employ in DrScheme. We establish basic properties of the model (type soundness, etc.) and illustrate the usefulness of contract checking with examples from DrScheme's code base.We believe that the development of an assertion system for higher-order functions serves two purposes. On one hand, the system has strong practical potential because existing type systems simply cannot express many assertions that programmers would like to state. On the other hand, an inspection of a large base of invariants may provide inspiration for the direction of practical future type system research.

DrScheme is a programming environment for Scheme. It fully integrates a graphics-enriched editor, a parser for multiple variants of Scheme, a functional read-eval-print loop, and an algebraic printer. The environment is especially useful for students, because it has a tower of syntactically restricted variants of Scheme that are designed to catch typical student mistakes and explain them in terms the students understand. The environment is also useful for professional programmers, due to its sophisticated programming tools, such as the static debugger, and its advanced language features, such as units and mixins. Beyond the ordinary programming environment tools, DrScheme provides an algebraic stepper, a context-sensitive syntax checker, and a static debugger. The stepper reduces Scheme programs to values, according to the reduction semantics of Scheme. It is useful for explaining the semantics of linguistic facilities and for studying the behavior of small programs. The syntax checker annotates programs with font and color changes based on the syntactic structure of the program. On demand, it draws arrows that point from bound to binding occurrences of identifiers. It also supports α-renaming. Finally, the static debugger provides a type inference system that explains specific inferences in terms of a value-flow graph, selectively overlaid on the program text.

The construction of interactive server-side Web applications differs substantially from the construction of traditional interactive programs. In contrast, existing Web programming paradigms force programmers to save and restore control state between user interactions. We present an automated transformation that converts traditional interactive programs into standard CGI programs. This enables reuse of existing software development methodologies. Furthermore, an adaptation of existing programming environments supports the development of Web programs.

Checking pre- and post-conditions of procedures and methods at runtime helps improve software reliability. In the procedural world, pre- and post-conditions have a straightforward interpretation. If a procedure's pre-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the procedure failed to compute the expected result.

Component-based software manufacturing has the potential to bring division-of-labor benefits to the world of software engineering. In order to make a market of software components viable, however, producers and consumers must agree on enforceable software contracts. In this paper, we show how to enforce contracts if components are manufactured from class and interface hierarchies. In particular, we focus on one style of contract: pre- and post-conditions. Programmers annotate class and interface methods with pre- and post-conditions and the run-time system checks these conditions during evaluation. These contracts guarantee that methods are called properly and provide appropriate results. In procedural languages, the use of pre- and post-condition contracts is well-established and studies have demonstrated its value. In object-oriented languages, however, assigning blame for pre- and post-condition failures poses subtle and complex problems. Specifically, assigning blame for malformed class and interface hierarchies is so difficult that none of the existing contract monitoring tools correctly assign blame for these failures. In this paper, we show how to overcome these problems in the context of Java. Our work is based on the notion of behavioral subtyping.

The MrEd virtual machine serves both as the implementation platform for the DrScheme programming environment, and as the underlying Scheme engine for executing expressions and programs entered into DrScheme's read-eval-print loop. We describe the key elements of the MrEd virtual machine for building a programming environment, and we step through the implementation of a miniature version of DrScheme in MrEd. More generally, we show how MrEd defines a high-level operating system for graphical programs.

Module and class systems have evolved to meet the demand for reuseable software components. Considerable effort has been invested in developing new module and class systems, and in demonstrating how each promotes code reuse. However, relatively little has been said about the interaction of these constructs, and how using modules and classes together can improve programs. In this paper, we demonstrate the synergy of a particular form of modules and classes---called units and mixins, respectively---for solving complex reuse problems in a natural manner.