The fully parenthesized Cambridge Polish syntax of Lisp, originally regarded as a temporary expedient to be replaced by more conventional syntax, possesses a peculiar virtue: A read procedure can parse it without knowing the syntax of any expressions, statements, definitions, or declarations it may represent. The result of that parsing is a list structure that establishes a standard representation for uninterpreted abstract syntax trees. This representation provides a convenient basis for macro processing, which allows the programmer to specify that some simple piece of abstract syntax should be replaced by some other, more complex piece of abstract syntax. As is well-known, this yields an abstraction mechanism that does things that procedural abstraction cannot, such as introducing new binding structures. The existence of that standard representation for uninterpreted abstract syntax trees soon led Lisp to a greater reliance upon macros than was common in other high-level languages. The importance of those features is suggested by the ten pages devoted to macros in an earlier ACM HOPL paper, “The Evolution of Lisp.” However, na'ive macro expansion was a leaky abstraction, because the movement of a piece of syntax from one place to another might lead to the accidental rebinding of a program’s identifiers. Although this problem was recognized in the 1960s, it was 20 years before a reliable solution was discovered, and another 10 before a solution was discovered that was reliable, flexible, and efficient. In this paper, we summarize that early history with greater focus on hygienic macros, and continue the story by describing the further development, adoption, and influence of hygienic and partially hygienic macro technology in Scheme. The interplay between the desire for standardization and the development of new algorithms is a major theme of that story. We then survey the ways in which hygienic macro technology has been adapted into recent non-parenthetical languages. Finally, we provide a short history of attempts to provide a formal account of macro processing.

We present a complete reasoning principle for contextual equivalence in an untyped probabilistic language. The language includes continuous (real-valued) random variables, conditionals, and scoring. It also includes recursion, since the standard call-by-value fixpoint combinator is expressible. We demonstrate the usability of our characterization by proving several equivalence schemas, including familiar facts from lambda calculus as well as results specific to probabilistic programming. In particular, we use it to prove that reordering the random draws in a probabilistic program preserves contextual equivalence. This allows us to show, for example, that (let x = e 1 in let y = e 2 in e 0 ) = ctx (let y = e 2 in let x = e 1 in e 0 ) (provided x does not occur free in e 2 and y does not occur free in e 1 ) despite the fact that e 1 and e 2 may have sampling and scoring effects.

Many languages use syntactic sugar to define parts of their surface language in terms of a smaller core. Thus some properties of the surface language, like its scoping rules , are not immediately evident. Nevertheless, IDEs, refactorers, and other tools that traffic in source code depend on these rules to present information to users and to soundly perform their operations. In this paper, we show how to lift scoping rules defined on a core language to rules on the surface, a process of scope inference . In the process we introduce a new representation of binding structure---scope as a preorder---and present a theoretical advance: proving that a desugaring system preserves α-equivalence even though scoping rules have been provided only for the core language. We have also implemented the system presented in this paper.

Abstract Current systems for safely manipulating values containing names only support simple binding structures for those names. As a result, few tools exist to safely manipulate code in those languages for which name problems are the most challenging. We address this problem with Romeo, a language that respects α-equivalence on its values, and which has access to a rich specification language for binding, inspired by attribute grammars. Our work has the complex-binding support of David Herman's λ m , but is a full-fledged binding-safe language like Pure FreshML.

Current languages for safely manipulating values with names only support term languages with simple binding syntax. As a result, no tools exist to safely manipulate code written in those languages for which name problems are the most challenging. We address this problem with Romeo, a language that respects α-equivalence on its values, and which has access to a rich specification language for binding, inspired by attribute grammars. Our work has the complex-binding support of David Herman's λm, but is a full-fledged binding-safe language like Pure FreshML.

Fine-grained concurrent data structures are crucial for gaining performance from multiprocessing, but their design is a subtle art. Recent literature has made large strides in verifying these data structures, using either atomicity refinement or separation logic with rely-guarantee reasoning. In this paper we show how the ownership discipline of separation logic can be used to enable atomicity refinement, and we develop a new rely-guarantee method that is localized to the definition of a data structure. We present the first semantics of separation logic that is sensitive to atomicity, and show how to control this sensitivity through ownership. The result is a logic that enables compositional reasoning about atomicity and interference, even for programs that use fine-grained synchronization and dynamic memory allocation.

If we represent a λ-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from β-reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently im

We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation leads to smaller and more tractable relations than does the method of Sumii and Pierce [31]. In particular, our method allows one to write down a bisimulation relation directly in cases where [31] requires an inductive specification, and where the principle of local invariants [22] is inapplicable. Our method can also express examples with higher-order functions, in contrast with the most widely known previous methods [4, 22, 32] which are limited in their ability to deal with such examples. The bisimulation conditions are derived by manually extracting proof obligations from a hypothetical direct proof of contextual equivalence.

Past attempts to relate two well-known models of backtracking computation have met with only limited success. We relate these two models using logical relations. We accommodate higher-order values and infinite computations. We also provide an operational semantics, and we prove it adequate for both models.

A characteristic of aspect-oriented programming, as embodied in Aspect J, is the use of advice and point cuts to define behavior that crosscuts the structure of the rest of the code. The events during execution at which advice may execute are called join points . A pointcut is a set of join points. An advice is an action to be taken at the join points in a particular pointcut. In this model of aspect-oriented programming, join points are dynamic in that they refer to events during the flow of execution of the program.We give a denotational semantics for a minilanguage that embodies the key features of dynamic join points, pointcuts, and advice. This is the first semantics for aspect-oriented programming that handles dynamic join points and recursive procedures. It is intended as a baseline semantics against which future correctness results may be measured.

No abstract available.

We consider the question of how a Continuation-Passing-Style (CPS) transformation changes the flow analysis of a program. We present an algorithm that takes the least solution to the flow constraints of a program and constructs in linear time the least solution to the flow constraints for the CPS-transformed program. Previous studies of this question used CPS transformations that had the effect of duplicating code, or of introducing flow sensitivity into the analysis. Our algorithm has the property that for a program point in the original program and the corresponding program point in the CPS-transformed program, the flow information is the same. By carefully avoiding both duplicated code and flow-sensitive analysis, we find that the most accurate analysis of the CPS-transformed program is neither better nor worse than the most accurate analysis of the original. Thus a compiler that needed flow information after CPS transformation could use the flow information from the original program to annotate some program points, and it could use our algorithm to find the rest of the flow information quickly, rather than having to analyze the CPS-transformed program.

Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a multi-pass optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize and prove the soundness of these analyses using small-step operational semantics. We also prove that any sound liveness analysis induces a correct program transformation.

A trampolined program is organized as a single loop in which computations are scheduled and their execution allowed to proceed in discrete steps. Writing programs in trampolined style supports primitives for multithreading without language support for continuations. Various forms of trampolining allow for different degrees of interaction between threads. We present two architectures based on an only mildly intrusive trampolined style. Concurrency can be supported at multiple levels of granularity by performing the trampolining transformation multiple times.

We present a domain-specific language for specifying recursive traversals of object structures, for use with the visitor pattern. Traversals are traditionally specified as iterations, forcing the programmer to adopt an imperative style, or are hard-coded into the program or visitor. Our proposal allows a number of problems best approached by recursive means to be tackled with the visitor pattern, while retaining the benefits of a separate traversal specification.

A useless variable is one whose value contributes nothing to the final outcome of a computation. Such variables are unlikely to occur in human-produced code, but may be introduced by various program transformations. We would like to eliminate useless parameters from procedures and eliminate the corresponding actual parameters from their call sites. This transformation is the extension to higher-order programming of a variety of dead-code elimination optimizations that are important in compilers for first-order imperative languages.

We introduce a method for proving the correctness of transformations of programs in languages like Scheme and ML. The method consists of giving the programs a denotational semantics in an operationally-based term model in which interaction is the basic observable, and showing that the transformation is meaning-preserving. This allows us to consider correctness for programs that interact with their environment without terminating, and also for transformations that change the internal store behavior of the program. We illustrate the technique on one of the Meyer-Sieber examples, and we use it to prove the correctness of assignment elimination for Scheme. The latter is an important but subtle step for Scheme compilers; we believe ours is the first proof of its correctness.

Abstract We present an O(n 3 ) time type inference algorithm for a type system with a largest type Τ , a smallest type ⊥, and the usual ordering between function types. The algorithm infers type annotations of least shape, and it works equally well for recursive types. For the problem of typability, our algorithm is simpler than the one of Kozen, Palsberg, and Schwartzbach for type inference without ⊥. This may be surprising, especially because the system with ⊥ is strictly more powerful.

We consider the problem of lightweight closure conversion, in which multiple procedure call protocols may coexist in the same code. A lightweight closure omits bindings for some of the free variables of the procedure that is represents. Flow analysis is used to match the protocol expected by each procedure and the protocol used at its possible call sites. We formulate the flow analysis as a deductive system that generates a labeled transition system and a set of constraints. We show that any solution to the constraints justifies the resulting transformation. Some of the techniques used are similar to those of abstract interpretation, but others appear to be novel.

We study a type system with a notion of subtyping that involves a largest type ⊤, a smallest type ⊥, atomic coercions between base types, and the usual ordering of function types. We prove that any λ-term typable in this system is strongly normalizing, which solves an open problem of Thatte. We also prove that the fragment without ⊥ types has strictly fewer terms. This demonstrates that ⊥ adds power to a type system.

We consider the problem of selective and lightweight closure conversion, in which multiple procedure-calling protocols may coexist in the same code. Flow analysis is used to match the protocol expected by each procedure and the protocol used at each of its possible call sites. We formulate the flow analysis as the solution of a set of constraints, and show that any solution to the constraints justifies the resulting transformation. Some of the techniques used are suggested by those of abstract interpretation, but others arise out of alternative approaches.

Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for the incorporating flow analyses into verified compilers.

Abstract Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for incorporating flow analyses into verified compilers.

A proof that a simple compiler correctly uses the static properties in its symbol table is presented. This is done by regarding the target code produced by the compiler as a syntactic variant of a lambda -term. In general, this lambda -term C may not be equal to the semantics S of the source program: they need to equal only when information in the symbol table is valid. Rules of inference for conditional lambda -judgements are presented, and their soundness is proven. These rules are then used to prove the correctness of a simple compiler that relies on a symbol table. The form of the proof suggests that such proofs may be largely mechanizable.>

The author shows that the type inference problem for a lambda calculus with records, including a record concatenation operator, is decidable. He shows that this calculus does not have principal types but does have finite complete sets of type, that is, for any term M in the calculus, there exists an effectively generable finite set of type schemes such that every typing for M is an instance of one of the schemes in the set. The author shows how a simple model of object-oriented programming, including hidden instance variables and multiple inheritance, may be coded in this calculus. The author concludes that type inference is decidable for object-oriented programs, even with multiple inheritance and classes as first-class values.>

An error has been pointed out in the author's paper (see Proc. 2nd IEEE Symp. on Logic in Computer Science, p.37-44 (1987)). It appears that there are programs without principal type schemes in the system in that paper.>

Three semantics-preserving transformations (static replacement, factoring, and combinator selection) are used to convert a continuation semantics into a formal description of a semantic analyzer and code generator. The result of this derivation is a compilation algorithm which performs type checking before code generation so that type-checking instructions are not generated in the target code. Both the flow analysis and the resulting optimizations are proved correct with respect to the original definition of the source language. The proof consists of showing that all restructuring transformations preserve the semantics of the source language. This transformational approach can be extended to derive correctness proofs of other flow analysis and code optimization techniques.

This paper presents two new developments. First, it describes a “macro-by-example” specification language for syntactic abstractions in Lisp and related languages. This specification language allows a more declarative specification of macros than conventional macro facilities do by giving a better treatment of iteration and mapping constructs. Second, it gives a formal semantics for the language and a derivation of a compiler from the semantics. This derivation is a practical application of semantics-directed compiler development methodology.

It is a truism that most bugs are detected only at a great distance from their source. Although polymorphic type-checking systems like those in ML help greatly by detecting potential run-time type errors at compile-time, such systems are still not very helpful for locating the source of a type error. Typically, an error is reported only when the type-checker can proceed no further, even though the programmer's actual error may have occurred much earlier in the text. We describe an algorithm which appears to be quite helpful in isolating and explaining the source of type errors. The algorithm works by keeping track of the reasons the checker makes deductions about the types of variables.

We show how a programming language designer may embed the type structure of a programming language in the more robust type structure of the typed lambda calculus. This is done by translating programs of the language into terms of the typed lambda calculus. Our translation, however, does not always yield a well-typed lambda term. Programs whose translations are not well-typed are considered meaningless, that is, ill-typed. We give a conditionally type-correct semantics for a simple language with continuation semantics. We provide a set of static type-checking rules for our source language, and prove that they are sound and complete: that is, a program passes the typing rules if and only if its translation is well-typed. This proves the correctness of our static semantics relative to the well-established typing rules of the typed lambda-calculus.

In this paper we present a semantics for Milner-style polymorphism in which types are sets. The basic picture is that our programs are actually terms in a typed λ-calculus, in which the type information can be safely deleted from the concrete syntax. In order to allow for common programming constructs, we allow reflexive or infinite types, and we also allow opaque types, which have private representations.

In our paper [Wand 82a], we introduced a paradigm for compilation based on combinators. A program from a source language is translated (via a semantic definition) to trees of combinators; the tree is simplified (via associative and distributive laws) to a linear, assembly-language-like format: the compiler writer's virtual machine operates by simulating a reduction sequence of the simplified tree. The correctness of these transformations follows from general results about the λ-calculus. The code produced by such n generator is always tree-like. In this paper, the method is extended to produce target code with explicit loops. This is done by re-introducing variables into the terms of the target language in a restricted way, along with a structured binding operator.

We show how to analyze the denotational semantics for a programming language to obtain a compiler and a suitable target machine for the language. We do this by rewriting the equations using suitable combinators. The machine operates by simulating the reduction sequences for the combinator terms. The reduction sequences pass through certain standard forms, which become an architecture for the machine, and the combinators become machine instructions. Despite the abstract nature of its development, the machine greatly resembles a conventional one. The method is illustrated by a simple expression language with procedures and input-output.

Reynolds' technique for deriving interpreters is extended to derive compilers from continuation semantics.The technique starts by eliminating h-variables from the semantic equations through the introduction of special-purpose combinators.The semantics of a program phrase may be represented by a term built from these combinators.Then associative and distributive laws are used to simplify the terms.Last, a machine is built to interpret the simplified terms as the functions they represent.The combinators reappear as the instructions of this machine.The technique is illustrated with three examples.

Program transformations often revolve the generahzation of a function to take additional arguments It is shown that m many eases such an additional variable arises as a representation of the continuation or global context m which the function is evaluated.By considering continuations, local transformation strategies can take advantage of global knowledge The general results are followed by two examples' the a-fl tree pruning algorithm and an algorithm for the conversion of a propositional formula to conjunctive normal form

There exist structures for which Hoare's formal system for partial correctness is incomplete, even ff the entire first-order theory of the structure is included among the axioms This incompleteness occurs even if attention is restricted to structures with a solvable halting problem, and to programs which always halt on the structure The implications of this result for program proving are discussed

A structure A is presented for which Hoare's formal system for partial correctness is incomplete, even if the entire first-order theory of A is included among the axioms. It follows that the language of first-order logic is insufficient to express all loop invariants. The implications of this result for program-proving are discussed.

An inductive proof in mathematics may often be expressed as an algorithm and a proof that the algorithm is correct. Especially when the proof proceeds by cases, a recursive pattern-matching language, such as Hewitt's MATCHLESS, is a felicitous language for writing the algorithm. We use this idea to prove a new mathematical result, which itself is of interest in computer science. We define objects called k-models. Our main theorem is a necessary and sufficient condition for a k-model to be the restriction of a k+1-model.