Mitchell Wand

Northeastern University

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Daniel P. Friedman

Indiana University Bloomington

Patrick O'Keefe

New Jersey Institute of Technology

Paul Stansifer

Northeastern University

Aaron Turon

Max Planck Institute for Software Systems

Olin Shivers

Epic Systems (United States)

Theophilos Giannakopoulos

Systems and Technology Research (United States)

Vasileios Koutavas

Trinity College Dublin

Christopher T. Haynes

Queen Mary University of London

Jens Palsberg

University of California, Los Angeles

Paul Steckler

Northeastern University

Cooperative Institutions

Northeastern University

Massachusetts Institute of Technology

Universidad del Noreste

Indiana University Bloomington

Indiana University

University of California, Berkeley

Stanford University

University of Edinburgh

National University of Singapore

Rice University

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

Theories, Pre-Theories and Finite State Transformations on Trees

Mitchell Wand

Source

Cite

Citations (0)

Small bisimulations for reasoning about higher-order imperative programs

ACM SIGPLAN Notices (2006)

Vasileios Koutavas Mitchell Wand

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.

Bisimulation

Equivalence relation

10.1145/1111320.1111050

Cite

Citations (12)

On the correctness of the Krivine machine

Higher-Order and Symbolic Computation (2007)

Mitchell Wand

10.1007/s10990-007-9019-8

Cite

Citations (18)

Understanding aspects

ACM SIGPLAN Notices (2003)

Mitchell Wand

No abstract available.

10.1145/944746.944732

Cite

Citations (1)

Linear future semantics and its implementation

Science of Computer Programming (1987)

Stefan Kölbl Mitchell Wand

Formal semantics (linguistics)

Continuation

Action semantics

10.1016/0167-6423(87)90005-0

Cite

Citations (0)

A characterization of weakest preconditions

Journal of Computer and System Sciences (1977)

Mitchell Wand

Characterization

10.1016/s0022-0000(77)80006-8

Cite

Citations (21)

First-order identities as a defining language

Acta Informatica (1980)

Mitchell Wand

Type safety

Abstract data type

Programming language specification

Data type

Theory of computation

Algebraic specification

Type theory

10.1007/bf00286491

Cite

Citations (36)

Hygienic macro technology

Proceedings of the ACM on Programming Languages (2020)

William Clinger Mitchell Wand

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.

Macro

Representation

Abstraction

Programmer

Common Lisp

10.1145/3386330

Cite

Citations (2)

Romeo: A system for more flexible binding-safe programming

Journal of Functional Programming (2016)

Paul Stansifer Mitchell Wand

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.

Code (set theory)

10.1017/s0956796816000137

Cite

Citations (2)

Free, iteratively closed categories of complete lattices

Cahiers de topologie et géométrie différentielle catégoriques (1975)

Mitchell Wand

Source

Cite

Citations (1)