Mitchell Wand, Ryan Culpepper, {Theophilos Giannakopoulos}, and {Andrew Cobb}. Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion. 2018. submitted for publication.
Abstract: 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 the two expressions
let x = e1 in y
= e2 in e0
and
let y = e2 in x = e1 in e0
are contextually
equivalent (provided x does not occur free in x2 and y does not occur free in
x1), even though e1 and e2 may have sampling and scoring effects.
Justin Pombrio, Shriram Krishnamurthi, and Mitchell Wand. Inferring Scope through Syntactic Sugar. Proc. ACM Programming Languages, 1({ICFP}):44:1--44:28, 2017.
Abstract: 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.
Paul Stansifer and Mitchell Wand. Romeo: a system for more flexible binding-safe programming. Journal of Functional Programming, 26(e13), 2016. doi: {10.1017/S0956796816000137}. Preliminary version appeared in ICFP 2014.
Abstract: Current languages for safely manipulating values with names provide support only for term languages with simple binding syntax. As a result, no 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 alpha-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 lambda_m, but is a full-fledged binding-safe language like Pure FreshML.
Paul Stansifer and Mitchell Wand. Romeo: a system for more flexible binding-safe programming. In Proc. ACM SIGPLAN International Conference on Functional Programming, pages 53--65, 2014.
Abstract: Current languages for safely manipulating values with names provide support only for term languages with simple binding syntax. As a result, no 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 $\lambda_m$, but is a full-fledged binding-safe language like Pure FreshML.
Aaron Turon and Mitchell Wand. A separation logic for refining concurrent objects. In Proceedings ACM Symposium on Programming Languages, pages 247--258, January 2011.
Abstract: 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. The result is a comprehensive and tidy account of concurrent data refinement that clarifies and consolidates the existing approaches.
Aaron Turon and Mitchell Wand. A resource analysis of the pi-calculus. In Proceedings 27th Conf. on the Mathematical Foundations of Programming Semantics (MFPS), Electronic Notes in Computer Science, May 2011.
Abstract: We give a new treatment of the pi-calculus based on the semantic theory of separation logic, continuing a research program begun by Hoare and O'Hearn. Using a novel resource model that distinguishes between public and private ownership, we refactor the operational semantics so that sending, receiving, and allocating are commands that influence owned resources. These ideas lead naturally to two denotational models: one for safety and one for liveness. Both models are fully abstract for the corresponding observables, but more importantly both are very simple. The close connections with the model theory of separation logic (in particular, with Brookes's action trace model) give rise to a logic of processes and resources.
Paul Stansifer and Mitchell Wand. Parsing Reflective Grammars. In Workshop on Language Descriptions, Tools, and Applications (LDTA), pages 73--79, Saarbrucken, Germany, March 2011.
Abstract: Existing technology can parse arbitrary context-free grammars, but only a single, static grammar per input. In order to support more powerful syntax-extension systems, we propose reflective grammars, which can modify their own syntax during parsing. We demonstrate and prove the correctness of an algorithm for parsing reflective grammars. The algorithm is based on Earley's algorithm, and we prove that it performs asymptotically no worse than Earley's algorithm on ordinary context-free grammars.
Olin Shivers and Mitchell Wand. Bottom-up beta-reduction: uplinks and lambda-DAGs (journal version). Fundamenta Infomaticae, 103(1-4):247--287, July 2010.
Abstract: If we represent a lambda-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from beta-reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement beta-reduction in a bottom-up manner, thus avoiding combinatorial explosion in time required to search the term in a top-down fashion. We present an algorithm for performing beta-reduction on lambda terms represented as uplinked DAGs; describe its proof of correctness; discuss its relation to alternate techniques such as Lamping graphs, explicit-substitution calculi and director strings; and present some timings of an implementation. Besides being both fast and parsimonious of space, the algorithm is particularly suited to applications such as compilers, theorem provers, and type-manipulation systems that may need to examine terms inbetween reductions---ie, the ``readback'' problem for our representation is trivial. Like Lamping graphs, and unlike director strings or the suspension lambda-calculus, the algorithm functions by side-effecting the term containing the redex; the representation is not a ``persistent'' one. The algorithm additionally has the charm of being quite simple; a complete implementation of the data structure and algorithm is 180 lines of SML.
Aaron Turon and Mitchell Wand. A Separation Logic for the Pi-calculus. unpublished, July 2009.
Abstract: Reasoning about concurrent processes requires distinguishing communication from interference, and is especially difficult when the means of interaction change over time. We present a new logic for the pi-calculus that combines temporal and separation logic, and treats channels as resources that can be gained and lost by processes. The resource model provides a lightweight way to constrain interference. By interpreting process terms as formulas, our logic directly supports compositional reasoning.
Christos Dimoulas and Mitchell Wand. The Higher-Order Aggregate Update Problem. In Neil~D. Jones and Markus Muller Olm, editors, Verification, Model Checking, and Abstract Interpretation, 10th International Conference, volume 5403 of Lecture Notes in Computer Science, pages 44--58, Berlin, Heidelberg, and New York, January 2009. Springer-Verlag.
Abstract: We present a multi-pass interprocedural analysis and transformation for the functional aggregate update problem. Our solution handles untyped programs, including unrestricted closures and nested arrays. Also, it can handle programs that contain a mix of functional and destructive updates. Correctness of all the analyses and of the transformation itself is proved.
Dimitris Vardoulakis and Mitchell Wand. A Compositional Trace Semantics for Orc. In Coordination Models and Languages: 10th International Conference, COORDINATION 2008, Oslo, Norway, June 4-6, 2008, volume 5052 of Lecture Notes in Computer Science, pages 331--346, Berlin, Heidelberg, and New York, 2008. Springer-Verlag. http://dx.doi.org/10.1007/978-3-540-68265-3\_21.
Abstract: Orc (Kitchin, Cook, and Misra 2006) is a language for task orchestration. It has a small set of primitives, but is sufficient to express many useful programs succinctly. We show that the operational and denotational semantics given in Kitchin et al. (2006) do not agree, by giving counterexamples to their Theorems 2 and 3. We remedy this situation by providing new operational and denotational semantics with a better treatment of variable binding, and proving an adequacy theorem to relate them. Our semantics validates some useful equivalences between Orc processes; since the semantics is compositional these automatically become congruences. Last, we consider an alternative semantics that is insensitive to internal events.
David Herman and Mitchell Wand. A Theory of Hygienic Macros. In Programming Languages and Systems 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008., volume 4960 of Lecture Notes in Computer Science, pages 48--62, Berlin, Heidelberg, and New York, 2008. Springer-Verlag. http://dx.doi.org/10.1007/978-3-540-78739-6\_4.
Abstract: Hygienic macro systems automatically rename variables to prevent unintentional variable capture-- in short, they "just work." But hygiene has never been presented in a formal way, as a specification rather than an algorithm. According to folklore, the definition of hygienic macro expansion hinges on the preservation of alpha-equivalence. But the only known definition of alpha-equivalence for Scheme depends on the results of macro expansion! We break this circularity by introducing binding specifications for macros, permitting a definition of alpha-equivalence independent of expansion. We define a semantics for a first-order subset of Scheme macros and prove hygiene as a consequence of confluence.
Daniel~P. Friedman and Mitchell Wand. Essentials of Programming Languages. MIT Press, Cambridge, MA, third edition, 2008.
Mitchell Wand. On the Correctness of the Krivine Machine. Higher-Order and Symbolic Computation, 20(3):231--236, September 2007.
Abstract: We provide a short proof of the correctness of the Krivine machine by showing how it simulates weak head reduction.
Vasileios Koutavas and Mitchell Wand. Reasoning About Class Behavior. In Informal Workshop Record of FOOL 2007, January 2007.
Abstract: We present a sound and complete method for reasoning about contextual equivalence between different implementations of classes in an imperative subset of Java. To the extent of our knowledge this is the first such method for a language with unrestricted inheritance, where the context can arbitrarily extend classes to distinguish presumably equivalent implementations. Similar reasoning techniques for class-based languages don't consider inheritance at all, or forbid the context from extending related classes. Other techniques that do consider inheritance study whole-program equivalence. Our technique also handles public, protected, and private interfaces of classes, imperative fields, and invocations of callbacks. Using our technique we were able to prove equivalences in examples with higher-order behavior, where previous methods for functional calculi admit limitations. Furthermore we use our technique as a tool to understand the exact effect of inheritance on contextual equivalence. We do that by deriving conditions of equivalence for a language without inheritance and compare them to those we get after we extend the language with it. In a similar way we show that adding a cast operator is a conservative extension of the language.
Vasileios Koutavas and Mitchell Wand. Small Bisimulations for Reasoning About Higher-Order Imperative Programs. In Proceedings 33rd ACM Symposium on Programming Languages, pages 141--152, January 2006.
Abstract: 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 [2004]. In particular, our method allows one to write down a bisimulation relation directly in cases where Sumii and Pierce 2004 requires an inductive specification, and where the method of Pitts and Stark [1998] is inapplicable. Our method can also express examples with higher-order functions, in contrast with the most widely known previous methods [Sumii-Pierce 2005, Pitts-Stark 1998, Benton-Leperchey 2005], which are limited in their ability to deal with examples containing higher-order functions. The bisimulation conditions are derived by manually extracting proof obligations from a hypothetical direct proof of contextual equivalence.
Vasileios Koutavas and Mitchell Wand. Bisimulations for Untyped Imperative Objects. In Peter Sestoft, editor, Proc. ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 146--161, Berlin, Heidelberg, and New York, March 2006. Springer-Verlag.
Abstract: We present a sound and complete method for reasoning about contextual equivalence in the untyped, imperative object calculus of Abadi and Cardelli [1]. Our method is based on bisimulations, following the work of Sumii and Pierce [26, 27] and our own [15]. Using our method we were able to prove equivalence in more complex examples than the ones of Gordon, Hankin and Lassen [7] and Gordon and Rees [8]. We can also write bisimulations in closed form in cases where similar bisimulation methods [27] require an inductive specification. To derive our bisimulations we follow the same technique as we did in [15], thus indicating the extensibility of this method.
Olin Shivers and Mitchell Wand. Bottom-up beta-reduction: uplinks and lambda-DAGs. In Mooly Sagiv, editor, Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings, volume 3444 of Lecture Notes in Computer Science, Berlin, Heidelberg, and New York, 2005. Springer-Verlag. expanded version available as BRICS Technical Report RS-04-38, Department of Computer Science, University of {\AA}rhus.
Abstract: This paper presents a new representation of lambda-caluclus terms that allows for fast, space-efficient beta-reduction. This representation is surprisingly simple, and is based on two ideas: (1) representing terms as a directed acyclic graph, allowing sharing, and (2) using explicit backpointers from children to parents, allowing us to replace blind search with minimal, directed traversals. We discuss the formal correctness of the algorithm, compare it with alternate techniques, and present comparative timings of implementations. An appendix contains a complete annotated code listing of the core data structrues and algorithms, in Standard ML
Philippe Meunier, Robby Findler, Paul~A. Steckler, and Mitchell Wand. Selectors Make Analyzing Case-Lambda Too Hard. Higher-Order and Symbolic Computation, 18(3-4):245--269, December 2005.
Abstract: Flanagan's set-based analysis (SBA) uses selectors to choose data flowing through expressions. For example, the rng selector chooses the ranges of procedures flowing through an expression. The MrSpidey static debugger for PLT Scheme is based on Flanagan's formalism. In PLT Scheme, a case-lambda is a procedure with possibly several argument lists and clauses. When a case-lambda is applied at a particular call site, at most one clause is actually invoked, chosen by the number of actual arguments. Therefore, an analysis should propagate data only through appropriate case-lambda clauses. MrSpidey propagates data through all clauses of a case-lambda, lessening its usefulness as a static debugger. Wishing to retain Flanagan's framework, we extended it to better analyze case-lambda with rest parameters by annotating selectors with arity information. The resulting analysis gives strictly better results than MrSpidey. Unfortunately, the improved analysis is too expensive because of overheads imposed by the use of selectors. Nonetheless, a closure-analysis style SBA (CA-SBA) eliminates these overheads and can give comparable results within cubic time.
Mitchell Wand and Dale Vaillancourt. Relating Models of Backtracking. In Proc. ACM SIGPLAN International Conference on Functional Programming, pages 54--65, 2004.
Abstract: Past attempts to relate two well-known models of backtracking computatation 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.
Mitchell Wand, Gregor Kiczales, and Christopher Dutchyn. A Semantics for Advice and Dynamic Join Points in Aspect-Oriented Programming. TOPLAS, 26(5):890--910, September 2004. Earlier versions of this paper were presented at the 9th International Workshop on Foundations of Object-Oriented Languages, January 19, 2002, and at the Workshop on Foundations of Aspect-Oriented Languages (FOAL), April 22, 2002.
Abstract: A characteristic of aspect-oriented programming, as embodied in AspectJ, is the use of _advice_ to incrementally modify the behavior of a program. An advice declaration specifies an action to be taken whenever some condition arises during the execution of the program. The condition is specified by a formula called a _pointcut designator_ or _pcd_. The events during execution at which advice may be triggered are called _join points_. In this model of aspect-oriented programming, join points are dynamic in that they refer to events during the execution of the program. We give a denotational semantics for a minilanguage that embodies the key features of dynamic join points, pointcut designators, and advice.
Mitchell Wand. Understanding Aspects (Extended Abstract). In Proc. ACM SIGPLAN International Conference on Functional Programming, August 2003. Summary of invited talk to be given at ICFP 2003.
Abstract: We report on our adventures in the AOP community, and suggest a narrative to explain the main ideas of aspect-oriented programming. We show how AOP as currently practiced invalidates conventional modular program reasoning, and discuss a reconceptualization of AOP that we hope will allow an eventual reconciliation between AOP and modular reasoning.
Jens Palsberg and Mitchell Wand. CPS Transformation of Flow Information. Journal of Functional Programming, 13(5):905--923, September 2003.
Abstract: 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 the rest of the flow information quickly, rather than having to analyze the CPS-transformed program.
Mitchell Wand and Galen~B. Williamson. A Modular, Extensible Proof Method for Small-step Flow Analyses. In Daniel~Le M{\'e}tayer, editor, Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings, volume 2305 of Lecture Notes in Computer Science, pages 213--227, Berlin, Heidelberg, and New York, 2002. Springer-Verlag.
Abstract: We introduce a new proof technique for showing the correctness of 0CFA-like analyses with respect to small-step semantics. We illustrate the technique by proving the correctness of 0CFA for the pure lambda-calculus under arbitrary beta-reduction. This result was claimed by Palsberg in 1995; unfortunately, his proof was flawed. We provide a correct proof of this result, using a simpler and more general proof method. We illustrate the extensibility of the new method by showing the correctness of an analysis for the Abadi-Cardelli object calculus under small-step semantics.
Mitchell Wand and Karl Lieberherr. Navigating through Object Graphs Using Local Meta-Information. unpublished report, June 2002.
Abstract: Traversal through object graphs is needed for many programming tasks. We show how this task may be specified declaratively at a high level of abstraction, and we give a simple and intuitive semantics for such specifications. The algorithm is implemented in a Java library called DJ.
Mitchell Wand and William~D. Clinger. Set Constraints for Destructive Array Update Optimization. Journal of Functional Programming, 11(3):319--346, May 2001.
Abstract: 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 preliminary version of this paper appeared in ICCL '98.
Mitchell Wand. A Semantics for Advice and Dynamic Join Points in Aspect-Oriented Programming. In Proceedings of SAIG '01, Lecture Notes in Computer Science, Berlin, Heidelberg, and New York, September 2001. Springer-Verlag. invited talk.
Philippe Meunier, Robby Findler, Paul~A. Steckler, and Mitchell Wand. Selectors Make Analyzing Case-Lambda Too Hard. In Proc. Scheme 2001 Workshop, Technical Report: Informatique, Signaux et Systemes de Sophia-Antipolis, I3S/RT-2001-12-FR, pages 54--64, September 2001.
Abstract: Flanagan's set-based analysis (SBA) uses selectors to choose data flowing through expressions. For example, the rng selector chooses the ranges of procedures flowing through an expression. The MrSpidey static debugger for PLT Scheme is based on Flanagan's formalism. In PLT Scheme, a case-lambda is a procedure with possibly several argument lists and clauses. When a case-lambda is applied at a particular call site, at most one clause is actually invoked, chosen by the number of actual arguments. Therefore, an analysis should propagate data only through appropriate case-lambda clauses. MrSpidey propagates data through all clauses of a case-lambda, lessening its usefulness as a static debugger. Wishing to retain Flanagan's framework, we extended it to better analyze case-lambda with rest parameters by annotating selectors with arity information. The resulting analysis gives strictly better results than MrSpidey. Unfortunately, the improved analysis is too expensive because of overheads imposed by the use of selectors. Nonetheless, a closure-analysis style SBA (CA-SBA) eliminates these overheads and can give comparable results within cubic time.
Daniel~P. Friedman, Mitchell Wand, and Christopher~T. Haynes. Essentials of Programming Languages. MIT Press, Cambridge, MA, second edition, 2001.
Mitchell Wand and Igor Siveroni. Constraint Systems for Useless Variable Elimination. In Proceedings 26th ACM Symposium on Programming Languages, pages 291--302, 1999.
Abstract: 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. Shivers has presented such a transformation. We reformulate the transformation and prove its correctness. We believe that this correctness proof can be a model for proofs of other analysis-based transformations.
Mitchell Wand. Continuation-Based Multiprocessing Revisited. Higher-Order and Symbolic Computation, 12(3):283, October 1999.
Abstract: This is a short introduction to the republication of "Continuation-Based Multiprocessing," which originally appeared in the 1980 Lisp Conference.
Mitchell Wand. Continuation-Based Multiprocessing. Higher-Order and Symbolic Computation, 12(3):285--299, October 1999. Originally appeared in the 1980 Lisp Conference.
Abstract: Any multiprocessing facility must include three features: elementary exclusion, data protection, and process saving. While elementary exclusion must rest on some hardware facility (e.g. a test-and-set instruction), the other two requirements are fulfilled by features already present in applicative languages. Data protection may be obtained through the use of procedures (closures or funargs), and process saving may be obtained through the use of the CATCH operator. The use of CATCH, in particular, allows an elegant treatment of process saving.
We demonstrate these techniques by writing the kernel and some modules for a multiprocessing system. The kernel is very small. Many functions which one would normally expect to find inside the kernel are completely decentralized. We consider the implementation of other schedulers, interrupts, and the implications of these ideas for language design.
This paper originally appeared in the 1980 Lisp Conference.
Johan Ovlinger and Mitchell Wand. A Language for Specifying Recursive Traversals of Object Structures. In Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA`99), pages 70--81, November 1999.
Abstract: 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.
Steven~E. Ganz, Daniel~P. Friedman, and Mitchell Wand. Trampolined Style. In Proc. 1999 ACM SIGPLAN International Conference on Functional Programming, pages 18--27, Paris, September 1999.
Abstract: 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.
Mitchell Wand and William~D. Clinger. Set Constraints for Destructive Array Update Optimization. In Proc. IEEE Conf. on Computer Languages '98, pages 184--193. IEEE, April 1998.
Abstract: 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 highly non-trivial optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize the sondness of these analyses using small-step operational semantics. We have shown that all solutions to our set constraints are sound. We have also proved that any sound liveness analysis induces a correct program transformation.
Mitchell Wand. The Theory of Fexprs is Trivial. Lisp and Symbolic Computation, 10:189--199, 1998.
Abstract: We provide a very simple model of a reflective facility based on the pure lambda-calculus, and we show that its theory of contextual equivalence is trivial: two terms in the language are contextually equivalent iff they are alpha-congruent.
Jonathan~A. Rees, William~D. Clinger, et al. Revised{$^5$} Report on the Algorithmic Language Scheme. Higher-Order and Symbolic Computation, 11(1):7--104, August 1998. also appeared in SIGPLAN Notices 33:9, September 1998.
Mitchell Wand and Gregory~T. Sullivan. Denotational Semantics Using an Operationally-Based Term Model. In Proceedings 23rd ACM Symposium on Programming Languages, pages 386--399, 1997.
Abstract: 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 some 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.
Mitchell Wand. Types in Compilation: Scenes from an Invited Lecture. Invited talk at Workshop on Types in Compilation, held in conjunction with ICFP97, June 1997.
Abstract: We consider some of the issues raised by the use of typed intermediate languages in compilers for higher-order languages. After a brief introduction, we consider typed vs.\ untyped equivalences, the relation between type analysis and flow analysis, and methods for proving the corrrectness of analysis-based program transformations.
Paul~A. Steckler and Mitchell Wand. Lightweight Closure Conversion. ACM Transactions on Programming Languages and Systems, 19(1):48--86, January 1997. Original version appeared in Proceedings 21st ACM Symposium on Programming Languages, 1994.
Abstract: 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 it represents. 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 nalysis as a deductive system tht generates a labelled transition system and a set of constraints. We show that any solution to the constraints justifies the rsulting transformation. Some of the techniques used a similar to those of abstract interpretation, but others appear to be novel.
Jens Palsberg, Mitchell Wand, and Patrick O'Keefe. Type Inference with Non-Structural Subtyping. Formal Aspects of Computer Science, 9:49--67, 1997.
Abstract: We present an O(n^3) time type inference algorithm for a type system with a largest type \top, a smallest type \bot, and the usual ordering between function types. The algorithm infers type annotations of minimal size, 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 \bot. This may be surprising, especially because the system with \bot is strictly more powerful.
Jerzy Tiuryn and Mitchell Wand. Untyped Lambda-Calculus with Input-Output. In H. Kirchner, editor, Trees in Algebra and Programming: CAAP'96, Proc.~21st International Colloquium, volume 1059 of Lecture Notes in Computer Science, pages 317--329, Berlin, Heidelberg, and New York, April 1996. Springer-Verlag.
Abstract: We introduce an untyped lambda-calculus with input-output, based on Gordon's continuation-passing model of input-output. This calculus is intended to allow the classification of possibly infinite input-output behaviors, such as those required for servers or distributed systems. We define two terms to be operationally approximate iff they have similar behaviors in any context. We then define a notion of applicative approximation and show that it coincides with operational approximation for these new behaviors. Last, we consider the theory of pure lambda-terms under this notion of operational equivalence.
Gregory~T. Sullivan and Mitchell Wand. Incremental Lambda Lifting: An Exercise in Almost-Denotational Semantics. manuscript, November 1996.
Abstract: We prove the correctness of incremental lambda-lifting, an optimization that attempts to reduce the closure allocation overhead of higher-order programs by changing the scope of nested procedures. This optimization is invalid in the standard denotational semantics of Scheme, because it changes the storage behavior of the program. Our method consists of giving Scheme a denotational semantics in an operationally-based term model in which interaction is the basic observable. Lambda lifting is then shown to preserve meaning in the model.
Jonathan~G. Rossie, Daniel~P. Friedman, and Mitchell Wand. Modeling Subobject-based Inheritance. In Pierre Cointe, editor, Proc. European Conference on Object-Oriented Programming, volume 1098 of Lecture Notes in Computer Science, pages 248--274, Berlin, Heidelberg, and New York, July 1996. Springer-Verlag.
Abstract: A model of subobjects and subobject selection gives us a concise expression of key semantic relationships in a variety of inheritance-based languages. Subobjects and their selection have been difficult to reason about explicitly because they are not explicit in the languages that support them. The goal of this paper is to present a relatively simple calculus to describe subobjects and subobject selection explicitly. Rather than present any deep theorems here, the goal is to present a general calculus that can be used to explore the design of inheritance systems.
David Gladstein and Mitchell Wand. Compiler Correctness for Concurrent Languages. In Paolo Ciancarini and Chris Hankin, editors, Proc. Coordination '96 (Cesena, Italy), volume 1061 of Lecture Notes in Computer Science, pages 231--248, Berlin, Heidelberg, and New York, April 1996. Springer-Verlag.
Abstract: This paper extends previous work in compiler derivation and verification to languages with true-concurrency semantics. We extend the lambda-calculus to model process-centered concurrent computation, and give the semantics of a small language in terms of this calculus. We then define a target abstract machine whose states have denotations in the same calculus. We prove the correctness of a compiler for our language: the denotation of the compiled code is shown to be strongly bisimilar to the denotation of the source program, and the abstract machine running the compiled code is shown to be branching-bisimilar tothe source program's denotation.
Mitchell Wand and Gregory~T. Sullivan. A Little Goes a Long Way: A Simple Tool to Support Denotational Compiler-Correctness Proofs. Technical Report NU-CCS-95-19, Northeastern University College of Computer Science, November 1995.
Abstract: In a series of papers in the early 80's we proposed a paradigm for semantics-based compiler correctness. In this paradigm, the source and target languages are given denotational semantics in the same lambda-theory, so correctness proofs can be carried out within this theory. In many cases, the proofs have a highly structured form. We show how a simple proof strategy, based on an algorithm for alpha-matching, can be used to build a tool that can automate all the routine cases of these proofs.
Mitchell Wand, Patrick O'Keefe, and Jens Palsberg. Strong Normalization with Non-structural Subtyping. Mathematical Structures in Computer Science, 5(3):419--430, September 1995.
Abstract: We study a type system with a notion of subtyping that involves a largest type $\top$, a smallest type $\bot$, atomic coercions between base types, and the usual ordering of function types. We prove that any $\lambda$-term typable in this system is strongly normalizing; this solves an open problem of Thatte. We also prove that the fragment without $\bot$ types strictly fewer terms. This demonstrates that $\bot$ adds power to a type system.
Mitchell Wand. Compiler Correctness for Parallel Languages. In Functional Programming Languages and Computer Architecture, pages 120--134, June 1995.
Abstract: We present a paradigm for proving the correctness of compilers for languages with parallelism. The source language is given a denotational semantics as a compositional translation to a higher-order process calculus. The target language is also given a denotational semantics as a compositional translation to the same process calculus. We show the compiler is correct in that it preserves denotation up to bisimulation. The target language is also given an operational semantics, and this operational semantics is shown correct in the sense that it is branching-bisimilar to the denotational semantics of the target language. Together, these results show that for any program, the operational semantics of the target code is branching-bisimilar to the semantics of the source code.
Dino~P. Oliva, John~D. Ramsdell, and Mitchell Wand. The VLISP Verified PreScheme Compiler. Lisp and Symbolic Computation, 8(1/2):111--182, 1995.
Abstract: This paper describes a verified compiler for PreScheme, the implementation language for the {\vlisp} run-time system. The compiler and proof were divided into three parts: A transformational front end that translates source text into a core language, a syntax-directed compiler that translates the core language into combinator-based tree-manipulation language, and a linearizer that translates combinator code into code for an abstract stored-program machine with linear memory for both data and code. This factorization enabled different proof techniques to be used for the different phases of the compiler, and also allowed the generation of good code. Finally, the whole process was made possible by carefully defining the semantics of {\vlisp} PreScheme rather than just adopting Scheme's. We believe that the architecture of the compiler and its correctness proof can easily be applied to compilers for languages other than PreScheme.
Joshua~D. Guttman and Mitchell Wand, editors. VLISP: A Verified Implementation of Scheme. Kluwer, Boston, 1995. Originally published as a special double issue of the journal {\it Lisp and Symbolic Computation} (Volume 8, Issue 1/2).
Abstract: The VLISP project undertook to verify rigorously the implementation of a programming language. The project began at The MITRE Corporation in late 1989, under the company's Technology Program. The work was supervised by the Rome Laboratory of the United States Air Force. Northeatern University became involved a year later. This research work has also been published as a special double issue of the journal {\it Lisp and Symbolic Computation} (Volume 8, Issue 1/2).
Joshua Guttman, John Ramsdell, and Mitchell Wand. VLISP: A Verified Implementation of Scheme. Lisp and Symbolic Computation, 8(1/2):5--32, 1995.
Abstract: The Vlisp project showed how to produce a comprehensively verified implementation for a programming language, namely Scheme. This paper introduces two more detailed studies on Vlisp. It summarizes the basic techniques that were used repeatedly throughout the effort. It presents scientific conclusions about the applicability of the these techniques as well as engineering conclusions about the crucial choices that allowed the verification to succeed.
Mitchell Wand and Zheng-Yu Wang. Conditional Lambda-Theories and the Verification of Static Properties of Programs. Information and Computation, 113(2):253--277, 1994. Preliminary version appeared in {\lics{5th}}, 1990, pp.~321-332.
Abstract: We present a proof that a simple compiler correctly uses the static properties in its symbol table. We do this by regarding the target code produced by the compiler as a syntactic variant of a \l-term. In general, this \l-term $C$ may not be equal to the semantics $S$ of the source program: they need be equal only when information in the symbol table is valid. We formulate this relation as a {\it {conditional \l-judgement}\/} $\Gbar \imp S = C$, where \Gbar\ is a formula that represents the invariants implicit in symbol table \G. We present rules of inference for conditional \l-judgements and prove their soundness. We then use these rules 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.
Mitchell Wand and Paul Steckler. Tracking Available Variables for Lightweight Closures. In Proceedings of Atlantique Workshop on Semantics-Based Program Manipulation, pages 63--70. University of Copenhagen DIKU Technical Report 94/12, 1994.
Mitchell Wand and Paul Steckler. Selective and Lightweight Closure Conversion. In Conf. Rec. 21th ACM Symp. on Principles of Prog. Lang., pages 435--445, 1994. Revised version appeared in {\em TOPLAS 19}:1, January, 1997, pp. 48-86.
Abstract: 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.
Mitchell Wand. Type Inference for Objects with Instance Variables and Inheritance. In Carl Gunter and John~C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming, pages 97--120. MIT Press, 1994. Originally appeared as Northeastern University College of Computer Science Technical Report NU-CCS-89-2, February, 1989.
Abstract: We show how to construct a complete type inference system for object systems with protected instance variables, publicly accessible methods, first-class classes, and single inheritance. This is done by extending Remy's scheme for polymorphic record typing to allow potentially infinite label sets, and interpreting objects in the resulting language.
Paul Steckler and Mitchell Wand. Selective Thunkification. In Baudouin~Le Charlier, editor, Static Analysis: First International Static Analysis Symposium, volume 864, pages 162--178. Springer-Verlag, Berlin, Heidelberg, and New York, September 1994.
Abstract: Recently, Amtoft presented an analysis and transformation for mapping typed call-by-name programs to call-by-value equivalents. Here, we present a comparable analysis and transformation for untyped programs using dataflow analysis. In the general case, the transformation generates thunks for call site operands of a call-by-name program. Using strictness information derived as part of a larger flow analysis, we can determine that some operands are necessarily evaluated under call-by-name, so the transformation does not need to generate thunks for them. The dataflow analysis is formulated as the solution to a set of constraints. We show that any solution to the constraints is sound, and that any such solution justifies the resulting transformation.
Mitchell Wand. Specifying the Correctness of Binding-Time Analysis. Journal of Functional Programming, 3(3):365--387, July 1993. Preliminary version appeared in {\it Conf. Rec. 20th ACM Symp. on Principles of Prog. Lang.\/} (1993), 137--143.
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.
Jerzy Tiuryn and Mitchell Wand. Type Reconstruction with Recursive Types and Atomic Subtyping. In {CAAP '93: 18th Colloquium on Trees in Algebra and Programming}, July 1993.
Abstract: We consider the problem of type reconstruction for \l-terms over a type system with recursive types and atomic subsumptions. This problem reduces to the problem of solving a finite set of inequalities over infinite trees. We show how to solve such inequalities by reduction to an infinite but well-structured set of inequalities over the base types. This infinite set of inequalities is solved using \Buchi\ automata. The resulting algorithm is in {\em DEXPTIME}. This also improves the previous {\em NEXPTIME} upper bound for type reconstruction for finite types with atomic subtyping. We show that the key steps in the algorithm are {\em PSPACE}-hard.
Mitchell Wand and Dino~P. Oliva. Proving the Correctness of Storage Representations. In {\lfp{1992}}, pages 151--160, 1992.
Abstract: Conventional techniques for semantics-directed compiler de\-ri\-vation yield abstract machines that manipulate trees. However, in order to produce a real compiler, one has to represent these trees in memory. In this paper we show how the technique of {\em {storage-layout relations}} (introduced by Hannan \cite{Hannan}) can be applied to verify the correctness of storage representations in a very general way. This technique allows us to separate denotational from operational reasoning, so that each can be used when needed. As an example, we show the correctness of a stack implementation of a language including dynamic catch and throw. The representation uses static and dynamic links to thread the environment and continuation through the stack. We discuss other uses of these techniques.
Mitchell Wand and Patrick~M. O'Keefe. Type Inference for Partial Types is Decidable. In B. Krieg Br{\"u}ckner, editor, European Symposium on Programming '92, volume 582 of Lecture Notes in Computer Science, pages 408--417, Berlin, Heidelberg, and New York, 1992. Springer-Verlag.
Abstract: The type inference problem for partial types, introduced by Thatte \cite{Thatte}, is the problem of deducing types under a subtype relation with a largest element \O\ and closed under the usual antimonotonic rule for function types. We show that this problem is decidable by reducing it to a satisfiability problem for type expressions over this partial order and giving an algorithm for the satisfiability problem. The satisfiability problem is harder than the one conventionally given because comparable types may have radically different shapes.
Mitchell Wand. Lambda Calculus. In S.C. Shapiro, editor, Encyclopedia of Artificial Intelligence, pages 760--761. Wiley-Inter\-science, 2nd edition, 1992.
Mitchell Wand. Correctness of Procedure Representations in Higher-Order Assembly Language. In S. Brookes, editor, Proceedings Mathematical Foundations of Programming Semantics '91, volume 598 of Lecture Notes in Computer Science, pages 294--311. Springer-Verlag, Berlin, Heidelberg, and New York, 1992.
Abstract: Higher-order assembly language (HOAL) generalizes combinator-based target languages by allowing free variables in terms to play the role of registers. We introduce a machine model for which HOAL is the assembly language, and prove the correctness of a compiler from a tiny language into HOAL. We introduce the notion of a lambda-representation, which is an abstract binding operation, show how some common representations of procedures and continuations can be expressed as lambda-representations. Last, we prove the correctness of a typical procedure-calling convention in this framework.
Dino~P. Oliva and Mitchell Wand. A Verified Run-Time Structure for Pure PreScheme. Technical Report NU-CCS-92-97, Northeastern University College of Computer Science, 1992.
Abstract: This document gives a summary of activities under MITRE Corporation Contract Number F19628-89-C-0001. It gives an operational semantics of an abstract machine for Pure PreScheme and of its implementation as a run-time structure on an Motorola 68000 microprocessor. The relationship between these two models is stated formally and proved.
Dino~P. Oliva and Mitchell Wand. A Verified Compiler for Pure PreScheme. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, February 1992.
Abstract: This document gives a summary of activities under MITRE Contract Number F19628-89-C-001. It gives a detailed denotational specification of the language Pure Pre\-Scheme. A bytecode compiler, derived from the semantics, is presented, followed by proofs of correctness of the compiler with respect to the semantics. Finally, an assembler from the bytecode to an actual machine architecture is shown.
Daniel~P. Friedman, Mitchell Wand, and Christopher~T. Haynes. Essentials of Programming Languages. MIT Press, Cambridge, MA, 1992.
Mitchell Wand and Patrick O'Keefe. Automatic Dimensional Inference. In J.L. Lassez and G.D. Plotkin, editors, Computational Logic: in honor of J. Alan Robinson, pages 479--486. MIT Press, 1991.
Abstract: While there have been a number of proposals to integrate dimensional analysis into existing compilers, it appears that no one has made the easy observation that dimensional analysis fits neatly into the pattern of ML-style type inference. In this paper we show how to add dimensions to the simply-typed lambda calculus, and we show that every typable dimension-preserving term has a principal type. The principal type is unique up to a choice of basis.
Mitchell Wand. Type Inference for Record Concatenation and Multiple Inheritance. Information and Computation, 93:1--15, 1991. Preliminary version appeared in {\it Proc. 4th IEEE Symposium on Logic in Computer Science\/} (1989), 92--97.
Abstract: We show that the type inference problem for a lambda calculus with records, including a record concatenation operator, is decidable. We show that this calculus does not have principal types, but does have finite complete sets of types: 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 the schemes in the set. We show how a simple model of object-oriented programming, including hidden instance variables and multiple inheritance, may be coded in this calculus. We conclude that type inference is decidable for object-oriented programs, even with multiple inheritance and classes as first-class values.
Margaret Montenyohl and Mitchell Wand. Correctness of Static Flow Analysis in Continuation Semantics. Science of Computer Programming, 16:1--18, 1991. Preliminary version appeared in {\popl{15th}} (1988), 204--218.
Boleslaw Ciesielski and Mitchell Wand. Using the Theorem Prover Isabelle-91 to Verify a Simple Proof of Compiler Correctness. Technical Report NU-CCS-91-20, Northeastern University College of Computer Science, December 1991.
William~D. Clinger, J. Rees, et al. Revised Report on the Algorithmic Language Scheme. Lisp Pointers, 4(3):1--55, July-September 1991. Has also appeared as MIT, Indiana University and University of Oregon technical reports.
Mitchell Wand. A Short Proof of the Lexical Addressing Algorithm. Information Processing Letters, 35:1--5, 1990.
Abstract: The question of how to express binding relations, and in particular, of proving the correctness of lexical addressing techniques, has been considered primarily in the context of compiler correctness proofs. Here we consider the problem in isolation. We formulate the connections between three different treatments of variables in programming language semantics: the environment coding, the natural coding, and the lexical-address coding (sometimes called the Frege coding, the Church coding, and the deBruijn coding, respectively). By considering the problem in isolation, we obtain shorter and clearer proofs. The natural coding seems to occupy a central place, and the other codings are proved equivalent by reference to it.
Mitchell Wand and Patrick~M. O'Keefe. On the Complexity of Type Inference with Coercion. In Conf. on Functional Programming Languages and Computer Architecture, 1989.
Abstract: We consider the following problem: Given a partial order $(C, \le)$ of base types and coercions between them, a set of constants with types generated from $C$, and a term $M$ in the lambda calculus with these constants, does $M$ have a typing with this set of types? This problem abstracts the problem of typability over a fixed set of base types and coercions ({\it e.g.}\ int $\le$ real, or a fixed set of coercions between opaque data types). We show that in general, the problem of typability of lambda-terms over a given partially-ordered set of base types is NP-complete. However, if the partial order is known to be a tree, then the satisfiability problem is solvable in (low-order) polynomial time. The latter result is of practical importance, as trees correspond to the coercion structure of single-inheritance object systems.
Mitchell Wand. The Register-Closure Abstract Machine: A Machine Model to Support {CPS} Compiling. Technical Report NU-CCS-89-24, Northeastern University College of Computer Science, Boston, MA, July 1989.
Abstract: We present a new abstract machine model for compiling languages based on their denotational semantics. In this model, the output of the compiler is a lambda-term which is the higher-order abstract syntax for an assembly language program. The machine operates by reducing these terms. This approach is well-suited for generating code for modern machines with many registers. We discuss how this approach can be used to prove the correctness of compilers, and how it improves on our previous work in this area.
Mitchell Wand. From Interpreter to Compiler via Higher-Order Abstract Assembly Language. Technical report, Northeastern University College of Computer Science, 1989.
Abstract: In this paper, we give a case study of transforming an interpreter into a compiler. This transformation improves on our previous work through the use of {\it {higher-order abstract assembly language}\/}. Higher-order abstract assembly language (or HOAL) uses a Church-style, continuation-passing encoding of machine operations. This improves on the use of combinator-based encoding in allowing a direct treatment of register usage, and thereby giving the compiler writer a clearer idea of how to incorporate new constructs in the source language or machine. For example, it allows a denotational exposition of stack layouts. We show how to do the transformation for a simple language, for a language with procedures, and for a compiler using lexical addresses.
Margaret Montenyohl and Mitchell Wand. Incorporating Static Analysis in a Semantics-Based Compiler. Information and Computation, 82:151--184, 1989.
Abstract: We show how restructuring a denotational definition leads to a more efficient compiling algorithm. 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 compiling algorithm derived below performs type checking before code generation so that type-checking instructions may be omitted from the target code. The optimized code is proved correct with respect to the original definition of the source language. The proof consists of showing that all transformations preserve the semantics of the source language.
Richard~P. Gabriel et al. Draft Report on Requirements for a Common Prototyping System. SIGPLAN Notices, 24(3):93--165, March 1989.
Mitchell Wand and Daniel~P. Friedman. The Mystery of the Tower Revealed: A Non-Reflective Description of the Reflective Tower. Lisp and Symbolic Computation, 1(1):11--37, 1988. Reprinted in {\it Meta-Level Architectures and Reflection} (P. Maes and D. Nardi, eds.) North-Holland, Amsterdam, 1988, pp. 111--134. Preliminary version appeared in {\it Proc. 1986 ACM Conf. on Lisp and Functional Programming,\/} 298--307.
Abstract: In an important series of papers [8,9], Brian Smith has discussed the nature of programs that know about their text and the context in which they are executed. He called this kind of knowledge reflection. Smith proposed a programming language, called 3-LISP, which embodied such self-knowledge in the domain of metacircular interpreters. Every 3-LISP program is interpreted by a metacircular interpreter, also written in 3-LISP. This gives rise to a picture of an infinite tower of metacircular interpreters, each being interpreted by the one above it. Such a metaphor poses a serious challenge for conventional modes of understanding of programming languages. In our earlier work on reflection [4], we showed how a useful species of reflection could be modeled without the use of towers. In this paper, we give a semantic account of the reflective tower. This account is self-contained in the sense that it does not employ reflection to explain reflection.
Matthias Felleisen, Mitchell Wand, Daniel~P. Friedman, and Bruce~F. Duba. Abstract Continuations: A Mathematical Semantics for Handling Functional Jumps. In Proc. 1988 ACM Conf. on Lisp and Functional Programming, pages 52--62, 1988.
Abstract: Continuation semantics is the traditional mathematical formalism for specifying the semantics of imperative control facilities. Modern Lisp-like languages, however, contain advanced control structures like full functional jumps and control delimiters for which continuation semantics is insufficient. We solve this problem by introducing an abstract domain of {\it rests\/} of computations with appropriate operations. Beyond being useful for the problem at hand, these {\it abstract continuations} turn out to have applications in a much broader context, \eg, the explication of parallelism, the modeling of control facilities in parallel languages, and the design of new control structures.
Mitchell Wand. A Simple Algorithm and Proof for Type Inference. Fundamenta Infomaticae, 10:115--122, 1987.
Abstract: We present a simple proof of Hindley's Theorem: that it is decidable whether a term of the untyped lambda calculus is the image under type-erasing of a term of the simply typed lambda calculus. The proof proceeds by a direct reduction to the unification problem for simple terms. This arrangement of the proof allows for easy extensibility to other type inference problems.
Mitchell Wand. Lambda Calculus. In S.C. Shapiro, editor, Encyclopedia of Artificial Intelligence, pages 441--443. Wiley-Inter\-science, 1987.
Mitchell Wand. Complete Type Inference for Simple Objects. In Proc. 2nd IEEE Symposium on Logic in Computer Science, pages 37--44, 1987. {Corrigendum}, \lics{3rd}, 1988, page 132.
Abstract: We consider the problem of strong typing for a model of object-oriented programming systems. These systems permit values which are records of other values, and in which fields inside these records are retrieved by name. We propose a type system which allows us to classify these kinds of values and to classify programs by the type of their result, as is usual in strongly-typed programming languages. Our type system has two important properties: it admits multiple inheritance, and it has a syntactically complete type inference system.
Stefan Kolbl and Mitchell Wand. Linear Future Semantics and its Implementation. Science of Computer Programming, 8:87--103, 1987.
Abstract: We describe linear future semantics, an extension of linear history semantics as introduced by Francez, Lehmann, and Pnueli, and show how it can be used to add multiprocessing to languages given by standard continuation semantics. We then demonstrate how the resulting semantics can be implemented. The implementation uses functional abstractions and non-determinacy to represent the sets of answers in the semantics. We give an example, using a semantic prototyping system based on the language Scheme.
Eugene~M. Kohlbecker and Mitchell Wand. Macro-by-Example: Deriving Syntactic Transformations from their Specifications. In {\popl{14th}}, pages 77--84, 1987.
Mitchell Wand. Finding the Source of Type Errors. In Conf. Rec. 13th ACM Symp. on Principles of Prog. Lang., pages 38--43, 1986.
Jonathan~A. Rees, William~D. Clinger, et al. Revised{$^3$} Report on the Algorithmic Language Scheme. SIGPLAN Notices, 21(12):37--79, December 1986.
D.P Friedman, C.T. Haynes, and Mitchell Wand. Obtaining Coroutines with Continuations. J. of Computer Languages, 11(3/4):143--153, 1986.
Mitchell Wand. From Interpreter to Compiler: A Representational Derivation. In H. Ganzinger and N.D. Jones, editors, Workshop on Programs as Data Objects, volume 217 of Lecture Notes in Computer Science, pages 306--324. Springer-Verlag, Berlin, Heidelberg, and New York, 1985.
Mitchell Wand. Embedding Type Structure in Semantics. In {\popl{12th}}, pages 1--6, 1985.
Abstract: We show how a programming language designer may embed the type structure of 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.
Albert~R. Meyer and Mitchell Wand. Continuation Semantics in Typed Lambda-Calculi. In R. Parikh, editor, Logics of Programs (Brooklyn, June, 1985), volume 193 of Lecture Notes in Computer Science, pages 219--224. Springer-Verlag, Berlin, Heidelberg, and New York, 1985.
Abstract: This paper reports preliminary work on the semantics of the continuation transform. Previous work on the semantics of continuations has concentrated on untyped lambda-calculi and has used primarily the mechanism of inclusive predicates. Such predicates are easy to understand on atomic values, but they become obscure on functional values. In the case of the typed lambda-calculus, we show that such predicates can be replaced by retractions. The main theorem states that the meaning of a closed term is a retraction of the meaning of the corresponding continuationized term.
W. Clinger, D.P. Friedman, and Mitchell Wand. A Scheme for a Higher-Level Semantic Algebra. In J. Reynolds and M. Nivat, editors, Algebraic Methods in Semantics: Proceedings of the US-French Seminar on the Application of Algebra to Language Definition and Compilation, pages 237--250. Cambridge University Press, Cambridge, 1985.
Mitchell Wand. What is Lisp? American Mathematical Monthly, 91:32--42, 1984.
Mitchell Wand. A Types-as-Sets Semantics for {Milner}-style Polymorphism. In {\popl{11th}}, pages 158--164, 1984.
Mitchell Wand. A Semantic Prototyping System. In Proceedings ACM SIGPLAN '84 Compiler Construction Conference, pages 213--221, 1984.
Abstract: We have written a set of computer programs for testing and exercising programming language specifications given in the style of denotational semantics. The system is built largely in Scheme 84, a dialect of LISP that serves as an efficient lambda-calculus interpreter. The system consists of: a syntax-directed transducer, which embodies the principle of compositionality, a type checker, which is extremely useful in debugging semantic definitions, and an interface to the yacc parser-generator, which allows the system to use concrete syntax rather than the often cumbersome abstract syntax for its programs. In this paper, we discuss the design of the system, its implementation, and discuss its use.
Daniel~P. Friedman and Mitchell Wand. Reification: Reflection without Metaphysics. In {\lfp{1984}}, pages 348--355, August 1984.
Daniel~P. Friedman, Christopher~T. Haynes, and Mitchell Wand. Continuations and Coroutines: An Exercise in Metaprogramming. In {\lfp{1984}}, pages 293--298, August 1984.
Daniel~P. Friedman, Christopher~T. Haynes, Eugene Kohlbecker, and Mitchell Wand. The Scheme 84 Reference Manual. Technical Report 153, Indiana University Computer Science Department, Bloomington, IN, March 1984. Revised June 1985.
Mitchell Wand. A Semantic Algebra for Logic Programming. Technical Report 148, Indiana University Computer Science Department, Bloomington, IN, August 1983.
Mitchell Wand. Loops in Combinator-Based Compilers. Information and Computation, 57(2-3):148--164, 1983. Previously appeared in {\popl{10th}}, 1983, pages 190--196.
Abstract: 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 $\lambda$-calculus. The code produced by such a 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 also consider general conditions under which these transformations hold.
Mitchell Wand. Specifications, Models, and Implementations of Data Abstractions. Theoretical Computer Science, 20:3--32, 1982.
Mitchell Wand. Semantics-Directed Machine Architecture. In {\popl{9th}}, pages 234--241, 1982.
Mitchell Wand. Deriving Target Code as a Representation of Continuation Semantics. ACM Transactions on Programming Languages and Systems, 4(3):496--517, July 1982.
Mitchell Wand. SCHEME Version 3.1 Reference Manual. Technical Report 93, Indiana University Computer Science Department, Bloomington, IN, June 1980.
Mitchell Wand. Induction, Recursion, and Programming. North Holland, New York, 1980.
Mitchell Wand. First-Order Identities as a Defining Language. Acta Informatica, 14:337--357, 1980.
Mitchell Wand. Different Advice on Structuring Compilers and Proving Them Correct. Technical Report 95, Indiana University Computer Science Department, Bloomington, IN, September 1980.
Mitchell Wand. Continuation-Based Program Transformation Strategies. Journal of the ACM, 27:164--180, 1980.
Mitchell Wand. Continuation-Based Multiprocessing. In J. Allen, editor, Conference Record of the 1980 LISP Conference, pages 19--28, Palo Alto, CA, 1980. The Lisp Company. Republished by ACM.
Mitchell Wand. Fixed-Point Constructions in Order-Enriched Categories. Theoretical Computer Science, 8:13--30, 1979.
Mitchell Wand. Final Algebra Semantics and Data Type Extensions. Journal of Computer and Systems Science, 19:27--44, 1979.
Mitchell Wand and Daniel~P. Friedman. Compiling Lambda Expressions Using Continuations and Factorizations. Journal of Computer Languages, 3:241--263, 1978.
Mitchell Wand. A New Incompleteness Result for {Hoare}'s System. Journal of the ACM, 25:168--175, 1978.
Mitchell Wand. A Characterization of Weakest Preconditions. Journal of Computer and Systems Science, 15:209--212, 1977.
Mitchell Wand. Algebraic Theories and Tree Rewriting Systems. Technical Report 66, Indiana University Computer Science Department, Bloomington, IN, July 1977.
Stuart~C. Shapiro and Mitchell Wand. The Relevance of Relevance. Technical Report 46, Indiana University, November 1976.
D.P. Friedman, D.S. Wise, and Mitchell Wand. Recursive Programming Through Table Lookup. In Proc. 1976 ACM Symposium on Symbolic and Algebraic Computation, pages 85--89, 1976.
David~S. Wise, Daniel~P. Friedman, Stuart~C. Shapiro, and Mitchell Wand. Boolean-Valued Loops. BIT, 15:431--451, 1975.
Mitchell Wand. On the Recursive Sepcification of Data Types. In E. Manes, editor, Category Theory Applied to Computation and Control, volume 25 of Lecture Notes in Computer Science, pages 214--217. Springer-Verlag, Berlin, Heidelberg, and New York, 1975.
Mitchell Wand. Free, Iteratively Closed Categories of Complete Lattices. Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle, 16:415--424, 1975.
Mitchell Wand. An Algebraic Formulation of the Chomsky Hierarchy. In E. Manes, editor, Category Theory Applied to Computation and Control, volume 25 of Lecture Notes in Computer Science, pages 209--213. Springer-Verlag, Berlin, Heidelberg, and New York, 1975.
Mitchell Wand. An Unusual Application of Program-Proving. In Proc. 5th ACM Symposium on Theory of Computing, pages 59--66, Austin, TX, 1973.
Mitchell Wand. Mathematical Foundations of Formal Language Theory. PhD thesis, MIT, 1973. MIT Project MAC TR-108 (December, 1973).
Mitchell Wand. A Concrete Approach to Abstract Recursive Definitions. In Maurice Nivat, editor, Automata, Languages, and Programming, pages 331--345. North-Holland, Amsterdam, 1973.
Mitchell Wand. The Elementary Algebraic Theory of Generalized Finite Automata. Notices AMS, 19(2):A325, 1972.
Mitchell Wand. Theories, Pretheories, and Finite-State Transducers on Trees. Artificial Intellligence Memo 216, MIT, May 1971.