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

A Theory of Hygienic Macros

Springer eBooks (2008)

David Herman Mitchell Wand

Macro

10.1007/978-3-540-78739-6_4

Cite

Citations (40)

Correctness of static flow analysis in continuation semantics

Science of Computer Programming (1991)

Margaret Montenyohl Mitchell Wand

Continuation

Abstract Interpretation

10.1016/0167-6423(91)90021-o

Cite

Citations (0)

Loops in combinator-based compilers

Information and Control (1983)

Mitchell Wand

Combinatory logic

Associative property

Tree (set theory)

10.1016/s0019-9958(83)80041-2

Cite

Citations (12)

Bottom-Up beta-Substitution: Uplinks and lambda-DAGs

BRICS Report Series (2004)

Olin Shivers Mitchell Wand

Terms of the lambda-calculus are one of the most important data structures we have in computer science. Among their uses are representing program terms, advanced type systems, and proofs in theorem provers. Unfortunately, heavy use of this data structure can become intractable in time and space; the typical culprit is the fundamental operation of beta reduction. 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, the suspension lambda-calculus (SLC) 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 in-between reductions - i.e., 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 core data structures and algorithms is 180 lines of fairly straightforward SML.

Tree (set theory)

10.7146/brics.v11i38.21863

Cite

Citations (3)

Bottom-up fl-reduction: uplinks and ‚-DAGs (journal version)

Mitchell Wand

If we represent a ‚-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from fl-reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement fl-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 fl-reduction on ‚-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—i.e., the “readback” problem for our representation is trivial. Like Lamping graphs, and unlike director strings or the suspension ‚ 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.

Representation

Tree (set theory)

Source

Cite

Citations (0)

Preface

Mathematical Structures in Computer Science (1992)

Mitchell Wand

An abstract is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.

10.1017/s0960129500001523

Cite

Citations (0)

Final algebra semantics and data type extensions

Journal of Computer and System Sciences (1979)

Mitchell Wand

Abstract data type

Data type

Implementation

10.1016/0022-0000(79)90011-4

Cite

Citations (174)

Embedding type structure in semantics

Mitchell Wand

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.

System F

Dependent type

Type safety

10.1145/318593.318602

Cite

Citations (23)

Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion

arXiv (Cornell University) (2018)

Mitchell Wand Ryan Culpepper Theophilos Giannakopoulos Andrew H. Cobb

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$) is equivalent to (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.

Combinatory logic

System F

Logical equivalence

10.48550/arxiv.1807.02809

Cite

Citations (0)

On the recursive specification of data types

Lecture notes in computer science (1975)

Mitchell Wand

Abstract data type

Data type

10.1007/3-540-07142-3_85

Cite

Citations (14)