@preamble{
"\def\popl#1{{\it {Conf. Rec. #1 ACM Symposium on Principles of Programming Languages}\/}}
\def\lics#1{{\it Proc. #1 IEEE Symposium on Logic in Computer Science\/}}
\def\lfp#1{{\it Proc. #1 ACM Symposium on Lisp and Functional
Programming}}
\def\tr{Northeastern University College of Computer Science Technical Report NU-CCS-}
\def\mfcs#1{{\it Mathematical Foundations of Computer Science #1}}"
}
@string{lncs = "Lecture Notes in Computer Science"}
@string{popl = "Proceedings ACM Symposium on Programming Languages"}
@string{popl21 = "Proceedings 21st ACM Symposium on Programming
Languages"}
@string{popl23 = "Proceedings 23rd ACM Symposium on Programming Languages"}
@string{popl26 = "Proceedings 26th ACM Symposium on Programming Languages"}
@string{popl06 = "Proceedings 33rd ACM Symposium on Programming Languages"}
@string{icfp99 = "Proc. 1999 ACM SIGPLAN International Conference on Functional Programming"}
@string{icfp = "Proc. ACM SIGPLAN International Conference on
Functional Programming"}
#string{ftpdir = "ftp://ftp.ccs.neu.edu/pub/people/wand/papers/"}
@string{wwwdir = "http://www.ccs.neu.edu/home/wand/papers/"}
@string{ftpdir = wwwdir}
@string{springer = "Springer-Verlag"}
@string{springeraddr = "Berlin, Heidelberg, and New York"}
@string{hosc = "Higher-Order and Symbolic Computation"}
Mitchell Wand, ``Theories, Pretheories, and Finite-State Transducers
on Trees,'' MIT Artificial Intelligence Memo \#216 (May, 1971).
@TechReport{Wand71,
author = "Mitchell Wand",
title = "Theories, Pretheories, and Finite-State Transducers
on Trees",
institution = "MIT",
year = "1971",
type = "Artificial Intellligence Memo",
number = "216",
OPTaddress = "",
month = may,
OPTnote = ""
}
Mitchell Wand, ``The Elementary Algebraic Theory of Generalized Finite
Automata,'' {\it Notices AMS 19,\/} 2 (1972), A325.
@Article{Wand72,
author = "Mitchell Wand",
title = "The Elementary Algebraic Theory of Generalized Finite
Automata",
journal = "Notices AMS",
year = "1972",
volume = "19",
number = "2",
pages = "A325",
OPTmonth = "",
OPTnote = ""
}
Mitchell Wand, ``A Concrete Approach to Abstract Recursive
Definitions,'' in {\it Automata, Languages, and Programming\/} (M.
Nivat, ed.), North-Holland (1973), 331--345. {\it CR 14}) \#25,828.
@InCollection{Wand73,
author = "Wand, Mitchell",
title = "A Concrete Approach to Abstract Recursive Definitions",
booktitle = "Automata, Languages, and Programming",
publisher = "North-Holland",
year = "1973",
editor = "Maurice Nivat",
pages = "331--345",
address = "Amsterdam",
}
Mitchell Wand, ``An Unusual Application of Program-Proving,'' {\it
Proc. 5th ACM Symposium on Theory of Computing,\/} Austin (1973),
59--66. {\it MR 55} \#1860.
@InProceedings{Wand73a,
author = "Mitchell Wand",
title = "An Unusual Application of Program-Proving",
booktitle = "Proc. 5th ACM Symposium on Theory of Computing",
year = "1973",
pages = "59-66",
address = "Austin, TX",
}
Mitchell Wand, ``Mathematical Foundations of Formal Language Theory,''
(Dissertation) MIT Project MAC TR-108 (December, 1973).
Hmm, should this be a PhDThesis or a TechnicalReport ?
@PhDThesis{Wand73b,
author = "Mitchell Wand",
title = "Mathematical Foundations of Formal Language Theory",
school = "MIT",
year = "1973",
note = "MIT Project MAC TR-108 (December, 1973)"
}
Mitchell Wand, ``PLISP: ACTORS for the Masses,'' {\it Proc. 2nd
Computer Science Conference,\/} Detroit (February, 1974), 32.
Mitchell Wand, ``Teaching Elementary Programming Using Structured
Programming,'' {\it Proc. 1st IU Computer Network Conference on
Computer Related Curriculum Materials, \/} New Albany, Indiana (March,
1974), 135--137.
Mitchell Wand, ``An Algebraic Formulation of the Chomsky Hierarchy,''
{\it Category Theory Applied to Computation and Control\/} (E. Manes,
ed.), Lecture Notes in Computer Science 25, Springer-Verlag, Berlin
(1975), 209--213. {\it MR\/} {\bf 56}, \#1,834.
@InCollection{Wand75,
author = "Mitchell Wand",
title = "An Algebraic Formulation of the Chomsky Hierarchy",
booktitle = "Category Theory Applied to Computation and Control",
publisher = springer,
year = "1975",
series = lncs,
volume = 25,
editor = "E. Manes",
OPTchapter = "",
pages = "209-213",
address = springeraddr,
OPTmonth = "",
OPTnote = ""
}
Mitchell Wand, ``On the Recursive Specification of Data Types,'' {\it Ibid.,\/}
214--217. {\it MR\/} {\bf 51}, \#2273.
@InCollection{Wand75a,
author = "Mitchell Wand",
title = "On the Recursive Sepcification of Data Types",
booktitle = "Category Theory Applied to Computation and Control",
publisher = springer,
year = "1975",
series = lncs,
editor = "E. Manes",
volume = 25,
OPTchapter = "",
pages = "214-217",
address = springeraddr,
OPTmonth = "",
OPTnote = ""
}
Mitchell Wand, ``Free, Iteratively Closed Categories of Complete
Lattices,'' {\it Cahiers de Topologie et Geometrie Differentielle 16:4
\/} (1975), 415--424.
@Article{Wand75b,
author = "Wand, Mitchell",
title = "Free, Iteratively Closed Categories of Complete Lattices",
journal = "Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle",
year = "1975",
volume = "16",
pages = "415--424",
}
Mitchell Wand, ``Boolean-Valued Loops,'' with D. S. Wise,
D. P. Friedman and S. C. Shapiro, {\it BIT 15\/} (1975), 431--451.
@Article{WiseEtAl75,
author = "Wise, David S. and Friedman, Daniel P. and Shapiro,
Stuart C. and Wand, Mitchell",
title = "Boolean-Valued Loops",
journal = "BIT",
year = "1975",
volume = "15",
pages = "431--451",
}
Stuart C. Shapiro and Mitchell Wand, ``The Relevance of Relevance,''
Technical Report No. 46, Computer Science Department, Indiana
University, Bloomington, (November, 1976).
@TechReport{ShapiroWand76,
author = "Stuart C. Shapiro and Mitchell Wand",
title = "The Relevance of Relevance",
institution = "Indiana University",
year = "1976",
type = "Technical Report",
number = "46",
OPTaddress = "",
month = nov,
OPTnote = ""
}
D.P. Friedman, D.S. Wise, and M. Wand, ``Recursive Programming Through
Table Lookup,'' {\it Proc. 1976 ACM Symposium on Symbolic and
Algebraic Computation,\/} 85--89.
@InProceedings{FriedmanWiseWand76,
author = "D.P. Friedman and D.S. Wise and Mitchell Wand",
title = "Recursive Programming Through Table Lookup",
booktitle = "Proc. 1976 ACM Symposium on Symbolic and Algebraic Computation",
year = "1976",
OPTeditor = "",
pages = "85-89",
}
Mitchell Wand, ``Algebraic Theories and Tree Rewriting Systems,''
Technical Report No. 66, Computer Science Department, Indiana
University, Bloomington (July, 1977).
@TechReport{Wand77b,
author = "Wand, Mitchell",
title = "Algebraic Theories and Tree Rewriting Systems",
institution = "Indiana University Computer Science Department",
year = "1977",
type = "Technical Report",
number = "66",
address = "Bloomington, IN",
month = jul,
}
Mitchell Wand, ``A Characterization of Weakest Preconditions,'' {\it
J. Computer and System Sciences 15 \/} (1977), 209--212. {\it CR 19},
\#32,904. {\it MR\/} {\bf 57}, \#8,165.
@Article{Wand77a,
author = "Wand, Mitchell",
title = "A Characterization of Weakest Preconditions",
journal = "Journal of Computer and Systems Science",
year = "1977",
volume = "15",
pages = "209--212",
}
Mitchell Wand, ``A New Incompleteness Result for Hoare's System,''
{\it J. ACM 25 \/} (1978) 168--175. {\it MR\/} {\bf 56}, \#4,225;
{\it MR\/} {\bf 57}, \#14,589.
@Article{Wand78,
author = "Wand, Mitchell",
title = "A New Incompleteness Result for {Hoare}'s System",
journal = "Journal of the ACM",
year = "1978",
volume = "25",
pages = "168--175",
}
Mitchell Wand and Daniel P. Friedman, ``Compiling Lambda Expressions
Using Continuations and Factorizations,'' {\it J. of Computer
Languages 3\/} (1978) 241--263.
@Article{WandFriedman78,
author = "Wand, Mitchell and Friedman, Daniel P.",
title = "Compiling Lambda Expressions Using Continuations and
Factorizations",
journal = "Journal of Computer Languages",
year = "1978",
volume = "3",
pages = "241--263",
}
Mitchell Wand, ``Fixed-Point Constructions in Order-Enriched
Categories,'' {\it Theoretical Computer Science 8\/} (1979), 13--30.
{\it MR\/} {\bf 80}e:18005.
@Article{Wand79b,
author = "Wand, Mitchell",
title = "Fixed-Point Constructions in Order-Enriched Categories",
journal = "Theoretical Computer Science",
year = "1979",
volume = "8",
pages = "13--30",
URL = wwwdir # {wand-tcs-79.pdf},
}
Mitchell Wand, ``Final Algebra Semantics and Data Type Extensions,''
{\it J. Computer and System Sciences 19\/} (1979), 27--44. {\it MR\/}
{\bf 81}h:68015.
@Article{Wand79a,
author = "Wand, Mitchell",
title = "Final Algebra Semantics and Data Type Extensions",
journal = "Journal of Computer and Systems Science",
year = "1979",
volume = "19",
pages = "27--44",
}
Mitchell Wand, ``Continuation-Based Program Transformation
Strategies,'' {\it J. ACM 27\/} (1980), 164--180. {\it CR 21},
\#36,265. {\it MR\/} {\bf 80}m:68025.
@Article{Wand80a,
author = "Wand, Mitchell",
title = "Continuation-Based Program Transformation Strategies",
journal = "Journal of the ACM",
year = "1980",
volume = "27",
pages = "164--180",
}
Mitchell Wand, {\it Induction, Recursion, and Programming, \/} North
Holland, New York (1980), 202 pp. {\it CR 22} \#37,983 {\it MR\/} {\bf
81}i:68001.
@Book{Wand80b,
author = "Mitchell Wand",
title = "Induction, Recursion, and Programming",
publisher = "North Holland",
year = "1980",
OPTeditor = "",
OPTvolume = "",
OPTseries = "",
address = "New York",
OPTedition = "",
OPTmonth = "",
OPTnote = ""
}
Mitchell Wand, ``Scheme Version 3.1 Reference Manual,'' Technical
Report No. 93, Computer Science Department, Indiana University,
Bloomington (June, 1980).
@TechReport{Wand80d,
author = "Wand, Mitchell",
title = "SCHEME Version 3.1 Reference Manual",
institution = "Indiana University Computer Science Department",
year = "1980",
type = "Technical Report",
number = "93",
address = "Bloomington, IN",
month = jun,
}
Mitchell Wand, ``Continuation-Based Multiprocessing,'' {\it Proc. 1980 LISP
Conference,\/} pp. 19--28.
missing
@InProceedings{Wand80e,
author = "Wand, Mitchell",
title = "Continuation-Based Multiprocessing",
booktitle = "Conference Record of the 1980 LISP Conference",
year = "1980",
editor = "J. Allen",
pages = "19--28",
publisher = "The Lisp Company",
address = "Palo Alto, CA",
note = "Republished by ACM",
}
Mitchell Wand, ``First-Order Identities as a Defining Language,'' {\it Acta Informatica
14\/} (1980), 337--357. {\it CR 22} \#37,930.
missing
@Article{Wand80c,
author = "Wand, Mitchell",
title = "First-Order Identities as a Defining Language",
journal = "Acta Informatica",
year = "1980",
volume = "14",
pages = "337--357",
}
Mitchell Wand, ``Different Advice on Structuring Compilers and Proving Them Correct,''
Technical Report No. 95, Computer Science Department, Indiana University,
Bloomington (September, 1980).
missing
@TechReport{Wand80f,
author = "Wand, Mitchell",
title = "Different Advice on Structuring Compilers and Proving Them
Correct",
institution = "Indiana University Computer Science Department",
year = "1980",
type = "Technical Report",
number = "95",
address = "Bloomington, IN",
month = sep,
URL = wwwdir # {tr-95.pdf},
}
Mitchell Wand, ``Semantics-Directed Machine Architecture,'' {\it Conf. Rec. 9th ACM
Symp. on Principles of Prog. Lang.\/} (1982), 234--241.
~/papers/popl-82/paper.txt (in troff!!)
@InProceedings{Wand82b,
author = "Wand, Mitchell",
title = "Semantics-Directed Machine Architecture",
booktitle = "{\popl{9th}}",
year = "1982",
pages = "234--241",
}
Mitchell Wand, ``Specifications, Models, and Implementations of Data Abstractions,''
{\it Theoretical Computer Science 20 \/} (1982), 3--32. {\it MR\/} {\bf
83}i:68022.
missing
@Article{Wand82a,
author = "Wand, Mitchell",
title = "Specifications, Models, and Implementations of Data
Abstractions",
journal = "Theoretical Computer Science",
year = "1982",
volume = "20",
pages = "3-32",
}
Mitchell Wand, ``Deriving Target Code as a Representation of Continuation Semantics,''
{\it ACM Trans. on Prog. Lang. and Systems 4,\/} 3 (July, 1982), 496--517.
missing
@Article{Wand82c,
author = "Wand, Mitchell",
title = "Deriving Target Code as a Representation of
Continuation Semantics",
journal = "ACM Transactions on Programming Languages and Systems",
year = "1982",
volume = "4",
number = "3",
pages = "496--517",
month = jul,
}
Mitchell Wand, ``Loops in Combinator-Based Compilers,'' {\it Information and Control
57,\/} 2--3 (May/June, 1983), 148--164.
missing
@Article{Wand83a,
author = "Wand, Mitchell",
title = "Loops in Combinator-Based Compilers",
journal = "Information and Computation",
year = 1983,
volume = "57",
number = "2-3",
pages = "148--164",
OPTmonth = "",
note = "Previously appeared in {\popl{10th}}, 1983, pages
190--196",
source = {/proj/wand/old/popl83/ic.tex},
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, ``A Semantic Algebra for Logic Programming'' Technical
Report No. 148, Computer Science Department, Indiana University,
Bloomington, (August, 1983).
missing
@TechReport{Wand83c,
author = "Wand, Mitchell",
title = "A Semantic Algebra for Logic Programming",
institution = "Indiana University Computer Science Department",
year = "1983",
type = "Technical Report",
number = "148",
address = "Bloomington, IN",
month = aug,
}
Mitchell Wand, ``What is Lisp?'' {\it American Mathematical Monthly
91\/} (1984), 32--42.
@Article{Wand84,
author = "Mitchell Wand",
title = "What is Lisp?",
journal = "American Mathematical Monthly",
year = "1984",
volume = "91",
OPTnumber = "",
pages = "32-42",
OPTmonth = "",
OPTnote = ""
}
Mitchell Wand, ``A Types-as-Sets Semantics for Milner-style
Polymorphism'' {\it Conf. Rec. 11th ACM Symp. on Principles of
Prog. Lang.\/} (1984), 158--164.
missing
@InProceedings{Wand84b,
author = "Wand, Mitchell",
title = "A Types-as-Sets Semantics for {Milner}-style Polymorphism",
booktitle = "{\popl{11th}}",
year = "1984",
pages = "158--164",
}
Mitchell Wand, ``A Semantic Prototyping System'' {\it Proc. SIGPLAN '84 Symposium on
Compiler Construction,\/} (1984), 213--221.
~wand/sps/paper/paper.tex
@InProceedings{Wand84c,
author = "Wand, Mitchell",
title = "A Semantic Prototyping System",
booktitle = "Proceedings ACM SIGPLAN '84 Compiler Construction Conference",
year = "1984",
pages = "213--221",
URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/sigplan-84.dvi},
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."
}
\item ``Scheme 84 Reference Manual'' (with D.P. Friedman, C.T. Haynes, and E.
Kohlbecker) Technical Report No. 153, Computer Science Department, Indiana
University, Bloomington (February, 1984).
missing
@TechReport{Friedmanetal84,
author = "Friedman, Daniel P. and Haynes, Christopher T. and
Kohlbecker, Eugene and Wand, Mitchell",
title = "The Scheme 84 Reference Manual",
institution = "Indiana University Computer Science Department",
year = "1984",
type = "Technical Report",
number = "153",
month = mar,
note = "Revised June 1985",
address = "Bloomington, IN",
}
\item ``Continuations and Coroutines: An Exercise in Metaprogramming'' (with
D.P. Friedman and C.T. Haynes) {\it Proc. 1984 ACM Symposium on Lisp and
Functional Programming\/} (August, 1984), 293--298.
missing
@InProceedings{FriedmanHaynesWand84,
author = "Friedman, Daniel P. and Haynes, Christopher T. and
Wand, Mitchell",
title = "Continuations and Coroutines: An Exercise in Metaprogramming",
booktitle = "{\lfp{1984}}",
year = "1984",
pages = "293-298",
month = aug,
}
\item ``Reification: Reflection without Metaphysics'' (with D.P. Friedman) {\it
Proc. 1984 ACM Symposium on Lisp and Functional Programming\/} (August, 1984),
348--355.
~wand/corresp/steele.tex
@InProceedings{FriedmanWand84,
author = "Friedman, Daniel P. and Wand, Mitchell",
title = "Reification: Reflection without Metaphysics",
booktitle = "{\lfp{1984}}",
year = "1984",
pages = "348-355",
month = aug,
}
Mitchell Wand, ``Embedding Type Structure in Semantics'' {\it Conf. Rec. 12th ACM
Symp. on Principles of Prog. Lang.\/} (1985), 1--6.
@InProceedings{Wand85a,
author = "Wand, Mitchell",
title = "Embedding Type Structure in Semantics",
booktitle = "{\popl{12th}}",
year = "1985",
pages = "1--6",
source = {/proj/wand/old/popl85/paper.tex},
URL = {http://www.ccs.neu.edu/home/wand/papers/popl-85.ps},
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." }
\item ``Continuation Semantics in Typed Lambda-Calculi'' (with A. Meyer), {\it
Logics of Programs (Brooklyn, June, 1985)\/} (R. Parikh, ed.) Springer Lecture
Notes in Computer Science, vol. 193 (1985), pp. 219--224.
/proj/wand/old/conts/abstract.tex
@InCollection{MeyerWand85,
author = "Albert R. Meyer and Mitchell Wand",
title = "Continuation Semantics in Typed Lambda-Calculi",
booktitle = "Logics of Programs (Brooklyn, June, 1985)",
publisher = Springer,
year = "1985",
editor = "R. Parikh",
pages = "219--224",
address = springeraddr,
series = lncs,
volume = "193",
source = {/proj/wand/old/conts/abstract.tex},
URL = {http://www.ccs.neu.edu/home/wand/papers/meyer-wand-85.ps},
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."
}
\item ``A Scheme for a Higher-Level Semantic Algebra,'' with W. Clinger and
D.P. Friedman, {\it Algebraic Methods in Semantics: Proceedings of the
US-French Seminar on the Application of Algebra to Language Definition and
Compilation (Fontainebleau, France, June, 1982) \/} (J. Reynolds \&\ M. Nivat,
eds.) Cambridge University Press, Cambridge (1985), 237--250.
@InCollection{ClingerFriedmanWand85,
author = "W. Clinger and D.P. Friedman and Mitchell Wand",
title = "A Scheme for a Higher-Level Semantic Algebra",
booktitle = "Algebraic Methods in Semantics: Proceedings of the
US-French Seminar on the Application of Algebra to
Language Definition and Compilation",
publisher = "Cambridge University Press",
year = "1985",
editor = "J. Reynolds and M. Nivat",
OPTchapter = "",
pages = "237-250",
address = "Cambridge",
OPTmonth = "",
OPTnote = ""
}
Mitchell Wand, ``From Interpreter to Compiler: A Representational Derivation'' {\it
Workshop on Programs as Data Objects (Copenhagen, 1985)\/} (H. Ganzinger and
N.D. Jones, eds.), Springer Lecture Notes in Computer Science, Vol. 217, pp.
306--324.
~wand/rcam/ch9/bjorner.tex -- I don't think this is right.
@InCollection{Wand85b,
author = "Mitchell Wand",
title = "From Interpreter to Compiler: A Representational Derivation",
booktitle = "Workshop on Programs as Data Objects",
publisher = springer,
address = springeraddr,
series = lncs,
volume = 217,
year = "1985",
editor = "H. Ganzinger and N.D. Jones",
pages = "306-324",
}
Mitchell Wand, ``Finding the Source of Type Errors'' {\it Conf. Rec. 13th ACM Symp. on
Principles of Prog. Lang.\/} (1986) 38--43.
~wand/proj/old/popl86/paper.tex
@InProceedings{Wand86,
author = "Mitchell Wand",
title = "Finding the Source of Type Errors",
booktitle = "Conf. Rec. 13th ACM Symp. on Principles of Prog. Lang.",
year = "1986",
OPTeditor = "",
pages = "38-43",
source = "~wand/proj/old/popl86/paper.tex",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
OPTnote = ""
}
\item ``Obtaining Coroutines with Continuations'' (with D.P. Friedman and C.T.
Haynes) {\it J. of Computer Languages 11,\/} No. 3/4 (1986), 143--153
@Article{FriedmanHaynesWand86,
author = "D.P Friedman and C.T. Haynes and Mitchell Wand",
title = "Obtaining Coroutines with Continuations",
journal = "J. of Computer Languages",
year = "1986",
volume = "11",
number = "3/4",
pages = "143-153",
OPTmonth = "",
OPTnote = ""
}
\item ``Revised$^3$ Report on the Algorithmic Language Scheme'' (J. Rees, W.
Clinger, eds., with 17 others) {\it SIGPLAN Notices 21,\/} 12 (December,
1986), 37--79
missing
@Article{ReesClingerEtAl86,
author = "Rees, Jonathan A. and Clinger, William D. and others",
title = "Revised{$^3$} Report on the Algorithmic Language Scheme",
journal = "SIGPLAN Notices",
year = "1986",
volume = "21",
number = "12",
pages = "37--79",
month = dec,
}
\item ``Macro-by-Example: Deriving Syntactic Transformations from their
Specifications'' (with E. Kohl\-becker) {\it Conf. Rec. 14th ACM Symp. on
Principles of Prog. Lang.\/} (1987), 77--84.
~wand/old/mbe/paper.tex
@InProceedings{KohlbeckerWand87,
author = "Kohlbecker, Eugene M. and Wand, Mitchell",
title = "Macro-by-Example: Deriving Syntactic Transformations
from their Specifications",
booktitle = "{\popl{14th}}",
year = "1987",
pages = "77--84",
source = {~wand/old/mbe/paper.tex},
URL = {http://www.ccs.neu.edu/home/wand/papers/popl-87.dvi}
}
file://ftp.ccs.neu.edu/pub/people/wand/papers/popl-87.dvi".
\item ``Linear Future Semantics and its Implementation'' (with S. Kolbl) {\it
Science of Computer Programming 8\/} (1987), 87--103.
/proj/wand/old/stefan/all.tex
@Article{KolblWand87,
author = "Stefan Kolbl and Mitchell Wand",
title = "Linear Future Semantics and its Implementation",
journal = "Science of Computer Programming",
year = "1987",
volume = "8",
OPTnumber = "",
pages = "87-103",
OPTmonth = "",
OPTnote = "",
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."
}
Mitchell Wand, ``Lambda Calculus'' {\it Encyclopedia of Artificial Intelligence\/} (S.C.
Shapiro, ed.) Wiley-Inter\-science (1987), 441--443.
@InCollection{Wand87,
author = "Mitchell Wand",
title = "Lambda Calculus",
booktitle = "Encyclopedia of Artificial Intelligence",
publisher = "Wiley-Inter\-science",
year = "1987",
editor = "S.C. Shapiro",
OPTchapter = "",
pages = "441-443",
OPTaddress = "",
OPTmonth = "",
OPTnote = ""
}
Mitchell Wand, ``A Simple Algorithm and Proof for Type Inference'' {\it Fundamenta
Informaticae 10\/} (1987), 115--122.
~wand/types/simple/paper.tex
@Article{Wand87a,
author = "Mitchell Wand",
title = "A Simple Algorithm and Proof for Type Inference",
journal = "Fundamenta Infomaticae",
year = "1987",
volume = "10",
OPTnumber = "",
pages = "115-122",
OPTmonth = "",
OPTnote = "",
URL = {http://www.ccs.neu.edu/home/wand/papers/fundamenta-87.dvi},
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."
}
file://ftp.ccs.neu.edu/pub/people/wand/papers/fundamenta-87.dvi".
Mitchell Wand, ``Complete Type Inference for Simple Objects'' {\it Proc. 2nd IEEE
Symposium on Logic in Computer Science\/} (1987), 37--44.
~wand/types/records/paper.tex
~wand/papers/lics-87
@InProceedings{Wand87b,
author = "Mitchell Wand",
title = "Complete Type Inference for Simple Objects",
booktitle = "Proc. 2nd IEEE Symposium on Logic in Computer Science",
year = "1987",
OPTeditor = "",
pages = "37-44",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
note = "{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.",
URL = wwwdir # {wand-lics-87.pdf},
}
\item ``Abstract Continuations: A Mathematical Semantics for Handling
Functional Jumps'' (with M. Felleisen, D. Friedman, and B. Duba), {\it Proc.
1988 ACM Conf.\ on Lisp and Functional Programming}, 52--62.
~wand/people/matthias/bc/ac/ac.tex
~wand/people/matthias/bc/lfp/paper.tex
~wand/people/matthias/bc/ac/paper.tex
@InProceedings{FelleisenWandFriedmanDuba88,
author = "Matthias Felleisen and Mitchell Wand and Daniel P.
Friedman and Bruce F. Duba",
title = "Abstract Continuations: A Mathematical Semantics for
Handling Functional Jumps",
booktitle = "Proc. 1988 ACM Conf. on Lisp and Functional Programming",
year = "1988",
OPTeditor = "",
pages = "52-62",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
OPTnote = "",
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."
}
\item ``The Mystery of the Tower Revealed: A Non-Reflective Description of the
Reflective Tower'' (with D. Friedman) {\it Lisp and Symbolic Computation 1}
(1988) 11--37. 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.
missing
@Article{WandFriedman88,
author = "Mitchell Wand and Daniel P. Friedman",
title = "The Mystery of the Tower Revealed: A Non-Reflective
Description of the Reflective Tower",
journal = "Lisp and Symbolic Computation ",
year = "1988",
volume = "1",
number = "1",
pages = "11-37",
OPTmonth = jun,
note = "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."
}
\item ``Draft Report on Requirements for a Common Prototyping System'' (R. P.
Gabriel, ed., and 6 others) {\it SIGPLAN Notices 24}, 3 (March, 1989), 93--165.
~wand/merit/88.tex
@Article{Wand89,
author = "Richard P. Gabriel and others",
title = "Draft Report on Requirements for a Common Prototyping System",
journal = "SIGPLAN Notices",
year = "1989",
volume = "24",
number = "3",
pages = "93-165",
month = mar,
OPTnote = ""
}
\item ``Incorporating Static Analysis in a Semantics-Based Compiler'' (with M.
Montenyohl), {\it Information and Computation 82\/} (1989) 151--184.
@Article{MontenyohlWand89,
author = "Margaret Montenyohl and Mitchell Wand",
title = "Incorporating Static Analysis in a Semantics-Based Compiler",
journal = "Information and Computation",
year = "1989",
volume = "82",
OPTnumber = "",
pages = "151-184",
OPTmonth = "",
OPTnote = "",
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."
}
\item ``On the Complexity of Type Inference with Coercion,'' (with Patrick
O'Keefe), {\it {Conf. on Functional Programming Languages and Computer
Architecture}\/} (London, September, 1989).
~wand/types/coercions/paper.tex
@InProceedings{WandOkeefe89,
author = "Mitchell Wand and Patrick M. O'Keefe",
title = "On the Complexity of Type Inference with Coercion",
booktitle = "Conf. on Functional Programming Languages and
Computer Architecture",
year = "1989",
OPTeditor = "",
OPTpages = "293-298",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "London",
OPTmonth = sep,
OPTnote = "",
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 for CPS
Compiling,'' \tr 89-24.
~wand/rcam/hoal/abstract.tex
@TechReport{Wand89a,
author = "Wand, Mitchell",
title = "The Register-Closure Abstract Machine: A Machine
Model to Support {CPS} Compiling",
institution = "Northeastern University College of Computer Science",
year = "1989",
type = "Technical Report",
number = "NU-CCS-89-24",
address = "Boston, MA",
month = jul,
URL = wwwdir # {rcam-89.pdf},
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,'' \tr, 1989.
~wand/rcam/ch9/paper.tex
~wand/rcam/ch9/1989-paper.tex
@TechReport{Wand89b,
author = "Mitchell Wand",
title = "From Interpreter to Compiler via Higher-Order
Abstract Assembly Language",
institution = "Northeastern University College of Computer Science",
year = "1989",
type = "Technical Report",
OPTnumber = "",
OPTaddress = "",
OPTmonth = "",
OPTnote = "",
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."
}
Mitchell Wand, ``A Short Proof of the Lexical Addressing Algorithm,''
{\it {Information Processing Letters 35}\/} (1990), 1--5.
~wand/rcam/lexaddr/paper.tex
@Article{Wand89c,
author = "Wand, Mitchell",
title = "A Short Proof of the Lexical Addressing Algorithm",
journal = "Information Processing Letters",
year = "1990",
volume = "35",
pages = "1--5",
URL = {http://www.ccs.neu.edu/home/wand/papers/ipl-90.dvi},
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." }
file://ftp.ccs.neu.edu/pub/people/wand/papers/ipl-90.dvi.
\item ``Conditional Lambda-Theories and the Verification of Static Properties
of Programs,'' (with Z-Y Wang), \lics{5th} (1990), 321--332. Revised version,
\tr 90-24, to appear in {\it {Information and Computation 109}\/} (1994).
~wand/rcam/imper/journal2/paper.tex
@article{WandWang94,
author = "Wand, Mitchell and Wang, Zheng-Yu",
title = "Conditional Lambda-Theories and the Verification
of Static Properties of Programs",
journal = "Information and Computation",
year = "1994",
volume = "113",
number = "2",
pages = "253-277",
OPTmonth = "",
note = "Preliminary version appeared in {\lics{5th}}, 1990,
pp.~321-332.",
URL = {http://www.ccs.neu.edu/home/wand/papers/lics-90.dvi},
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." }
file://ftp.ccs.neu.edu/pub/people/wand/papers/lics-90.dvi".
\item
``Correctness of Static Flow Analysis in Continuation Semantics'' (with M.
Montenyohl) {\em {Science of Computer Programming 16}} (1991), 1--18.
Preliminary version appeared in {\it Conf. Rec. 15th ACM Symp. on Principles
of Prog. Lang.\/} (1988), 204--218.
@Article{MontenyohlWand91,
author = "Montenyohl, Margaret and Wand, Mitchell",
title = "Correctness of Static Flow Analysis in Continuation Semantics",
journal = "Science of Computer Programming",
year = "1991",
volume = "16",
pages = "1--18",
note = "Preliminary version appeared in {\popl{15th}} (1988), 204--218"
}
Mitchell Wand,
``Type Inference for Record Concatenation and Multiple Inheritance,'' {\it
{Information \&\ Computation 93}\/} (1991), 1--15. Preliminary version
appeared in {\it Proc. 4th IEEE Symposium on Logic in Computer Science\/}
(1989), 92--97.
@Article{Wand91,
author = "Wand, Mitchell",
title = "Type Inference for Record Concatenation and Multiple
Inheritance",
journal = "Information and Computation",
year = "1991",
volume = "93",
pages = "1--15",
note = " Preliminary version appeared in {\it Proc. 4th IEEE
Symposium on Logic in Computer Science\/} (1989), 92--97." ,
source = {~wand/types/mult/journal.tex},
URL = {http://www.ccs.neu.edu/home/wand/papers/ic-91.dvi},
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."
}
file://ftp.ccs.neu.edu/pub/people/wand/papers/ic-91.tex".
\item
``Automatic Dimensional Inference,'' (with Patrick O'Keefe), {\it
{Computational Logic: in honor of J. Alan Robinson}\/} ( J.-L.~Lassez and G.
D. Plotkin, eds.), MIT Press, (1991), pp. 479--486.
~wand/types/dimen/paper.tex
@InCollection{WandOKeefe91,
author = "Mitchell Wand and Patrick O'Keefe",
title = "Automatic Dimensional Inference",
booktitle = "Computational Logic: in honor of J. Alan Robinson",
publisher = "MIT Press",
year = "1991",
editor = "J.L. Lassez and G.D. Plotkin",
pages = "479-486",
URL = {http://www.ccs.neu.edu/home/wand/papers/dimensions.ps},
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,
``Correctness of Procedure Representations in Higher-Order Assembly
Language,'' {\it {Proc. MFPS '91}\/} (S. Brookes, ed.), Springer Lecture Notes
in Computer Science, Volume 598, (1992), pp. 294--311.
~wand/rcam/procs/paper.tex
@InCollection{WandMFPS,
author = "Wand, Mitchell",
title = "Correctness of Procedure Representations in Higher-Order
Assembly Language",
booktitle = "Proceedings Mathematical Foundations of Programming Semantics '91",
year = "1992",
editor = "S. Brookes",
series = lncs,
volume = "598",
pages = "294--311",
publisher = springer,
address = springeraddr,
URL = {http://www.ccs.neu.edu/home/wand/papers/mfps-91.dvi},
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." }
file://ftp.ccs.neu.edu/pub/people/wand/papers/mfps-91.dvi".
\item
``Using the Theorem Prover Isabelle-91 to Verify a Simple Proof of Compiler
Correctness,'' (with Boleslaw Ciesielski), \tr 91-20, December, 1991.
/proj/wand/bolek/add.shar [add.tex is unreadable]
@TechReport{CiesielskiWand91,
author = "Boleslaw Ciesielski and Mitchell Wand ",
title = "Using the Theorem Prover Isabelle-91 to Verify a
Simple Proof of Compiler Correctness",
institution = "Northeastern University College of Computer Science",
year = 1991,
OPTtype = "",
number = "NU-CCS-91-20",
OPTaddress = "",
month = dec,
OPTnote = "",
URL = {http://www.ccs.neu.edu/home/wand/papers/wand-ciesielski-91.dvi},
}
file://ftp.ccs.neu.edu/pub/people/wand/papers/wand-ciesielski-91.dvi".
Mitchell Wand, ``Lambda Calculus,'' in {\it Encyclopedia of Artificial
Intelligence\/} (2nd edition, S.C. Shapiro, ed.) Wiley-Inter\-science
(1992), pp. 760--761.
@InCollection{Wand92,
author = "Mitchell Wand",
title = "Lambda Calculus",
booktitle = "Encyclopedia of Artificial Intelligence",
publisher = "Wiley-Inter\-science",
year = "1992",
editor = "S.C. Shapiro",
edition = "2nd",
pages = "760-761",
}
@Book{FriedmanWandHaynes92,
author = "Daniel P. Friedman and Mitchell Wand and Christopher
T. Haynes",
title = "Essentials of Programming Languages",
publisher = "MIT Press",
year = "1992",
address = "Cambridge, MA",
URL = "http://www.cs.indiana.edu/eip/eopl.html",
}
\item
``A Verified Compiler for Pure PreScheme,'' (with Dino P. Oliva), \tr 92-5,
February, 1992.
/proj/wand/mitre/91report/report.tex
@TechReport{OlivaWand92,
author = "Dino P. Oliva and Mitchell Wand",
title = "A Verified Compiler for Pure PreScheme",
institution = "Northeastern University College of Computer Science",
year = "1992",
type = "Technical Report",
number = "NU-CCS-92-5",
OPTaddress = "",
month = feb,
OPTnote = "",
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."
}
\item
``Type Inference for Partial Types is Decidable,'' (with Patrick O'Keefe),
{\it {European Symposium on Programming '92}\/} (B. Krieg-Br\"uckner, ed.),
Springer Lecture Notes in Computer Science, Vol.~582, pp. 408--417.
~wand/types/partial/paper.tex
@InProceedings{WandOKeefe92,
author = "Mitchell Wand and Patrick M. O'Keefe",
title = "Type Inference for Partial Types is Decidable",
booktitle = "European Symposium on Programming '92",
year = 1992,
editor = "B. Krieg-Br{\"u}ckner",
pages = "408--417",
publisher = springer,
series = lncs,
volume = "582",
address = springeraddr,
URL = {http://www.ccs.neu.edu/home/wand/papers/esop-92.dvi},
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."
}
file://ftp.ccs.neu.edu/pub/people/wand/papers/esop-92.dvi".
\item
``Revised$^4$ Report on the Algorithmic Language Scheme,'' (W. Clinger and J.
Rees, eds, with 15 others), {\em {Lisp Pointers} 4},3 (July--September 1991),
1--55. Also has appeared as MIT, University of Oregon, and Indiana University
technical reports.
missing
@Article{ClingerReesetal91,
author = "William D. Clinger and J. Rees and others",
title = "Revised Report on the Algorithmic Language Scheme",
journal = "Lisp Pointers",
year = "1991",
volume = "4",
number = "3",
pages = "1-55",
month = "July-September",
note = "Has also appeared as MIT, Indiana University and
University of Oregon technical reports."
}
\item
``Proving the Correctness of Storage Representations,'' (with Dino P. Oliva),
{\it Proc. 1992 ACM Conf. on Lisp and Functional Programming,\/} 151--160.
~wand/rcam/stacks/paper.tex
@InProceedings{WandOliva92,
author = "Mitchell Wand and Dino P. Oliva",
title = "Proving the Correctness of Storage Representations",
booktitle = "{\lfp{1992}}",
year = "1992",
pages = "151--160",
URL = {http://www.ccs.neu.edu/home/wand/papers/lfp-92.dvi},
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."
}
file://ftp.ccs.neu.edu/pub/people/wand/papers/lfp-92.dvi".
\item
``A Verified Run-Time Structure for Pure PreScheme'' (with Dino P. Oliva),
final report for MITRE Contract F19628-89-C001, \tr 92-27, September, 1992.
/proj/wand/mitre/92report/report.tex
@TechReport{OlivaWand92a,
author = "Dino P. Oliva and Mitchell Wand",
title = "A Verified Run-Time Structure for Pure PreScheme",
institution = "Northeastern University College of Computer Science",
year = "1992",
type = "Technical Report",
number = "NU-CCS-92-97",
OPTaddress = "",
OPTmonth = sep,
OPTnote = "",
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."
}
\item
``Type Reconstruction with Recursive Types and Atomic Subtyping'' (with J.
Tiuryn), \tr 92-18, July, 1992; to appear in {\em {CAAP '93: 18th Colloquium
on Trees in Algebra and Programming}}, 1993.
~wand/types/circular/paper.tex
@InProceedings{TiurynWand93,
author = "Jerzy Tiuryn and Mitchell Wand",
title = "Type Reconstruction with Recursive Types and Atomic Subtyping",
booktitle = "{CAAP '93: 18th Colloquium on Trees in Algebra and Programming}",
year = 1993,
month = jul,
URL = {http://www.ccs.neu.edu/home/wand/papers/caap-93.dvi},
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."
}
file://ftp.ccs.neu.edu/pub/people/wand/papers/caap93.dvi".
\item
``Specifying the Correctness of Binding-Time Analysis,'' {\em {Journal of
Functional Programming 3}} (1993), 365--387. preliminary version appeared in
{\it Conf. Rec. 20th ACM Symp. on Principles of Prog. Lang.\/} (1993),
137--143.
~wand/peval/bta/journal.tex
@Article{Wand93,
author = "Mitchell Wand",
title = "Specifying the Correctness of Binding-Time Analysis",
journal = "Journal of Functional Programming",
year = "1993",
volume = "3",
number = "3",
pages = "365--387",
month = jul,
note = "Preliminary version appeared in {\it Conf. Rec. 20th ACM Symp. on Principles of Prog. Lang.\/} (1993),
137--143.",
URL = {http://www.ccs.neu.edu/home/wand/papers/jfp-93.dvi.Z},
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." }
file://ftop.ccs.neu.edu/pub/people/wand/papers/jfp-93.dvi.Z".
\item
``Selective and Lightweight Closure Conversion,'' (with P. Steckler), {\it
Conf. Rec. 21th ACM Symp. on Principles of Prog. Lang.\/} (1994), 435--445.
~wand/peval/closures/popl/paper.tex
@InProceedings{WandSteckler94,
author = "Mitchell Wand and Paul Steckler",
title = "Selective and Lightweight Closure Conversion",
booktitle = "Conf. Rec. 21th ACM Symp. on Principles of Prog. Lang.",
year = "1994",
OPTeditor = "",
pages = "435-445",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
note = "Revised version appeared in {\em TOPLAS 19}:1,
January, 1997, pp. 48-86.",
URL = {http://www.ccs.neu.edu/home/wand/papers/popl-94.dvi},
source = {~/wand/peval/closures/popl},
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."
}
\item
``Tracking Available Variables,'' (with Paul Steckler), presented at
Atlantique Workshop on Semantics-Based Program Manipulation, Portland, OR,
January, 1994
~wand/peval/closures/atlantique/abstract.tex
@InCollection{WandSteckler94b,
author = "Mitchell Wand and Paul Steckler",
title = "Tracking Available Variables for Lightweight Closures",
institution = "University of Copenhagen",
year = "1994",
booktitle = "Proceedings of Atlantique Workshop on Semantics-Based
Program Manipulation",
publisher = "University of Copenhagen DIKU Technical Report 94/12",
pages = "63-70",
URL = {http://www.ccs.neu.edu/home/wand/papers/atlantique-94.ps},
}
Mitchell Wand,
``Type Inference for Objects with Instance Variables and Inheritance,'' {\em
Theoretical Aspects of Object-Oriented Programming} (Carl Gunter and John
C. Mitchell, eds.), MIT Press, 1994, pp. 97--120. Originally appeared as
Northeastern University College of Computer Science Technical Report
NU-CCS-89-2, February, 1989.
~wand/types/objects/paper.tex
@Inproceedings{Wand89objects,
author = "Wand, Mitchell",
title = "Type Inference for Objects with Instance Variables and
Inheritance",
institution = "Northeastern University College of Computer Science",
year = "1994",
booktitle = "Theoretical Aspects of Object-Oriented Programming",
editor = "Carl Gunter and John C. Mitchell",
publisher = "MIT Press",
pages = "97-120",
note = "Originally appeared as Northeastern University College of
Computer Science Technical Report NU-CCS-89-2,
February, 1989.",
URL = {http://www.ccs.neu.edu/home/wand/papers/gunter-mitchell-94.dvi},
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." }
file://ftp.ccs.neu.edu/pub/people/wand/papers/gunter-mitchell-94.dvi".
\item
``A Verified Compiler for VLISP PreScheme,'' (with D. P. Oliva and J. D.
Ramsdell), submitted for publication.
/proj/wand/mitre/lasc/prescheme/old/ramsdell1/ps.tex
/proj/wand/mitre/lasc/prescheme/old/authors.tex
/proj/wand/mitre/lasc/prescheme/working/authors.tex
/proj/wand/mitre/lasc/prescheme/4-94/titlepage.tex
/proj/wand/mitre/lasc/prescheme/6-94/titlepage.tex
@Article{OlivaRamsdellWand95,
author = "Dino P. Oliva and John D. Ramsdell and Mitchell Wand",
title = "The VLISP Verified PreScheme Compiler",
journal = "Lisp and Symbolic Computation",
year = "1995",
URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc/prescheme.dvi},
volume = "8",
number = "1/2",
pages = "111-182",
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."
}
@Article{GuttmanRamsdellWand95,
author = "Joshua Guttman and John Ramsdell and Mitchell Wand",
title = "VLISP: A Verified Implementation of Scheme",
journal = "Lisp and Symbolic Computation",
year = "1995",
volume = "8",
number = "1/2",
pages = "5--32",
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.",
URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc/overview.dvi},
}
@TechReport{WandSullivan95,
author = "Mitchell Wand and Gregory T. Sullivan",
title = "A Little Goes a Long Way: A Simple Tool to Support
Denotational Compiler-Correctness Proofs",
year = "1995",
month = nov,
institution = "Northeastern University College of Computer Science",
number = "NU-CCS-95-19",
source = {~wand/unif/lfp/abstract.tex},
URL = {http://www.ccs.neu.edu/home/wand/papers/wand-sullivan-95.ps},
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."
}
\item
``Strong Normalization with Non-structural Subtyping'' (with P. M. O'Keefe and
J. Palsberg), \tr94-13, to appear in MSCS
~/types/sn/final.tex
@Article{WandOKeefePalsberg95,
author = "Mitchell Wand and Patrick O'Keefe and Jens Palsberg",
title = "Strong Normalization with Non-structural Subtyping",
journal = "Mathematical Structures in Computer Science",
year = 1995,
volume = "5",
number = "3",
pages = "419-430",
month = sep,
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.",
source = {~/types/sn/final.tex},
URL = "http://www.ccs.neu.edu/home/wand/papers/w-ok-p-94.dvi",
}
@Inproceedings{Wand95,
author = "Mitchell Wand",
title = "Compiler Correctness for Parallel Languages",
booktitle = "Functional Programming Languages and Computer
Architecture",
year = "1995",
month = jun,
pages = "120-134",
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. ",
source = "/proj/wand/parallel/compilers/",
URL = "http://www.ccs.neu.edu/home/wand/papers/parallel-compilers.ps",
}
@InCollection{StecklerWand94,
author = "Paul Steckler and Mitchell Wand",
title = "Selective Thunkification",
booktitle = "Static Analysis: First International Static Analysis
Symposium ",
publisher = springer,
year = "1994",
editor = "Baudouin Le Charlier",
volume = 864,
OPTchapter = "",
pages = "162-178",
address = springeraddr,
month = sep,
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.",
URL = "http://www.ccs.neu.edu/home/wand/papers/sas-94.ps",
}
#Unpublished{GladsteinWand95,
author = "David Gladstein and Mitchell Wand",
title = "Compiler Correctness for Concurrent Languages",
note = "submitted for publication",
year = "1995",
month = mar,
abstract = "This paper extends previous work in compier 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 denoations 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
to the source program's denotation.",
source = "/proj/wand/parallel/concurrent/paper.tex",
URL = "http://www.ccs.neu.edu/home/wand/papers/gladstein-wand-95.dvi",
}
@Book{GuttmanWand95,
title = "VLISP: A Verified Implementation of Scheme",
publisher = "Kluwer",
year = "1995",
editor = "Joshua D. Guttman and Mitchell Wand",
OPTvolume = "",
OPTseries = "",
address = "Boston",
OPTedition = "",
OPTmonth = "",
note = "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).",
URL = "ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc",
}
#Unpublished{TiurynWand95a,
author = "Jerzy Tiuryn and Mitchell Wand",
title = "Untyped Lambda-Calculus with Input-Output (Progress Report)",
note = "presented at Atlantique meeting, La Jolla",
year = "1995",
month = jun,
source = {/proj/wand/parallel/io/atlantique.tex},
URL = {http://www.ccs.neu.edu/home/wand/papers/tiuryn-wand-95a.ps},
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. We introduce a property,
called ``losslessness,'' which is a natural property
of any reasonable model of this calculus. We then
characterize the largest lossless precongruence that
refines simulation for this calculus.",
}
#Unpublished{TiurynWand95b,
author = "Jerzy Tiuryn and Mitchell Wand",
title = "Adding Input-Output to PCF (Technical Summary)",
note = "manuscript",
year = "1995",
month = jul,
source = {/proj/wand/tiuryn/pcf-io/},
URL = {http://www.ccs.neu.edu/home/wand/papers/tiuryn-wand-95b.ps},
abstract = "We extend Plotkin's PCF by adding monadic-style
input-output operations. This extension is intended
to allow the classification of possibly infinite
input-output behaviors, such as those required for
servers or distributed systems. We define a notion
of applicative approximation and show that it
coincides with operational equivalence for these new
behaviors. Last, we show that the new notion of
operational equivalence is a conservative extension
of the usual one.",
}
@InProceedings{TiurynWand96,
author = "Jerzy Tiuryn and Mitchell Wand",
title = "Untyped Lambda-Calculus with Input-Output",
year = "1996",
booktitle = {Trees in Algebra and Programming: CAAP'96, Proc.~21st
International Colloquium},
editor = {H. Kirchner},
pages = "317-329",
organization = "",
publisher = springer,
address = springeraddr,
series = lncs,
volume = 1059,
month = apr,
source = {/proj/wand/tiuryn/untyped/caap.tex},
URL = {http://www.ccs.neu.edu/home/wand/papers/caap-96.ps},
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."
}
#Unpublished{ClingerWand95,
author = "William D. Clinger and Mitchell Wand",
title = "Interprocedural Array Update Optimization is Sound",
note = "submitted for publication",
year = 1995,
month = oct,
abstract = "We consider a program transformation that introduces
imperative assignments into a language of
first-order, call-by-value recursion equations. We
formulate and prove the soundness not only of the
underlying analyses but also of the transformation.
The proof relies on the formulaton of the analyses as
set constraints, and on the use of several different
operational semantics.",
source = {/proj/wand/clinger/update/abstract.tex},
}
@InProceedings{RossieFriedmanWand96,
author = "Jonathan G. Rossie and Daniel P. Friedman and
Mitchell Wand",
title = "Modeling Subobject-based Inheritance",
booktitle = {Proc. European Conference on Object-Oriented Programming},
year = 1996,
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.",
editor = {Pierre Cointe},
volume = 1098,
series = lncs,
publisher = springer,
address = springeraddr,
month = jul,
pages = {248-274},
URL = {http://www.ccs.neu.edu/home/wand/papers/ecoop-96.ps},
source = {~wand/people/dan/jrossie/ecoop-96.ps}
}
#Unpublished{WandSullivan96,
author = "Mitchell Wand and Gregory T. Sullivan",
title = "An Extensional Metalanguage with I/O and a Dynamic Store",
note = "submitted for publication",
year = "1995",
month = dec,
abstract = "We introduce a typed metalanguage based on PCF that
includes I/O and store operations. We give an
applicative characterization of operational
equivalence for this language. Finally, we give an
example of a translation from an imperative
programming language into our metalanguage, and we
demonstrate how to use the theory of the metalanguge
to reason about terms in the source programming
language.",
URL = {http://www.ccs.neu.edu/home/wand/papers/wand-sullivan-95b.ps},
source = {/proj/wand2/gregs/papers/lics96/abstract.tex},
note = {superceded by WandSullivan97}
}
@InProceedings{GladsteinWand96,
author = {David Gladstein and Mitchell Wand},
title = {Compiler Correctness for Concurrent Languages},
booktitle = {Proc. Coordination '96 (Cesena, Italy)},
editor = {Paolo Ciancarini and Chris Hankin},
volume = 1061,
series = lncs,
year = 1996,
publisher = springer,
address = springeraddr,
month = apr,
pages = {231-248},
URL = {http://www.ccs.neu.edu/home/wand/papers/coord-96.ps},
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.},
source = {~wand/people/gladstein/concur-96.tar}
}
@article{StecklerWand97,
author = {Paul A. Steckler and Mitchell Wand},
title = {Lightweight Closure Conversion},
note = {Original version
appeared in } # popl21 #{, 1994},
journal = {ACM Transactions on Programming Languages and Systems},
year = {1997},
volume = {19},
number = {1}, month = jan,
pages = {48-86},
URL = {http://www.ccs.neu.edu/home/wand/papers/steckler-wand-97.ps},
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.},
source = {~/people/steckler},
}
@InProceedings{WandSullivan97,
author = {Mitchell Wand and Gregory T. Sullivan},
title = {Denotational Semantics Using an Operationally-Based
Term Model},
booktitle = popl23,
year = 1997,
pages = {386-399},
URL = {http://www.ccs.neu.edu/home/wand/papers/wand-sullivan-96b.ps},
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.},
source = {proj/gregs/popl97/},
}
@Unpublished{SullivanWand96,
author = {Gregory T. Sullivan and Mitchell Wand},
title = {Incremental Lambda Lifting: An Exercise in
Almost-Denotational Semantics},
note = {manuscript},
OPTkey = {},
year = {1996},
month = nov,
URL = ftpdir # {sullivan-wand-97.ps},
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.},
OPTsource = {},
OPTannote = {}
}
Wand 96 is now Wand98
article{Wand96,
author = {Mitchell Wand},
title = {The Theory of Fexprs is Trivial},
note = {to appear in {\it Lisp and Symbolic Computation}, 1998},
OPTkey = {},
year = {1996},
month = dec,
URL = ftpdir # {fexprs.ps},
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.},
source = {/proj/wand/reflect/},
OPTannote = {}
}
@Misc{Wand-tic-97,
OPTkey = {},
author = {Mitchell Wand},
title = {Types in Compilation: Scenes from an Invited Lecture},
howpublished = {Invited talk at Workshop on Types in Compilation,
held in conjunction with ICFP97},
year = {1997},
month = jun,
OPTnote = {},
URL = {http://www.ccs.neu.edu/home/wand/papers/tic-97.ps},
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. },
source = {~/proj/tic},
OPTannote = {}
}
@Article{PalsbergWandOKeefe97,
author = {Jens Palsberg and Mitchell Wand and Patrick O'Keefe},
title = {Type Inference with Non-Structural Subtyping},
journal = {Formal Aspects of Computer Science},
year = 1997,
volume = 9,
pages = {49-67},
URL = {http://www.ccs.neu.edu/home/wand/papers/p-w-ok-95.ps},
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.},
source = {~/people/palsberg/facs*},
annote = {originally appeared as BRICS Technical Report RC-95-33}
}
@InProceedings{WandClinger98,
author = {Mitchell Wand and William D. Clinger},
title = {Set Constraints for Destructive Array Update Optimization},
booktitle = {Proc. IEEE Conf. on Computer Languages '98},
year = 1998,
organization = {IEEE},
month = apr,
pages = {184-193},
URL = ftpdir # {iccl-98.ps},
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.},
source = {~/proj/clinger/small-step/ICCL/}
}
@Article{Wand98,
author = {Mitchell Wand},
title = {The Theory of Fexprs is Trivial},
journal = {Lisp and Symbolic Computation},
year = 1998,
volume = 10,
pages = {189-199},
URL = ftpdir # {fexprs.ps},
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.},
source = {/proj/wand/reflect/}
}
@InProceedings{WandSiveroni99,
author = {Mitchell Wand and Igor Siveroni},
title = {Constraint Systems for Useless Variable Elimination},
booktitle = popl26,
year = 1999,
pages = {291-302},
URL = ftpdir # {wand-siveroni99.ps},
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. },
source = {/proj/wand/igor/popl99/final/paper.tex}
}
#Article{KelseyClingerReesEtAl98,
author = "Rees, Jonathan A. and Clinger, William D. and others",
title = "Revised{$^5$} Report on the Algorithmic Language Scheme",
journal = "SIGPLAN Notices",
year = "1998",
volume = "33",
number = "9",
pages = "26-76",
month = sep,
}
@Article{KelseyClingerReesEtAl98,
author = {Rees, Jonathan A. and Clinger, William D. and others},
title = {Revised{$^5$} Report on the Algorithmic Language Scheme},
journal = {Higher-Order and Symbolic Computation},
year = 1998,
volume = 11,
number = 1,
month = aug,
pages = {7-104},
note = {also appeared in SIGPLAN Notices 33:9, September 1998}
}
@InProceedings{OvlingerWand99,
author = {Johan Ovlinger and Mitchell Wand},
title = {A Language for Specifying Recursive Traversals of Object
Structures},
booktitle = {Proceedings of the 1999 ACM SIGPLAN Conference on
Object-Oriented Programming, Systems,
Languages, and Applications (OOPSLA`99)},
pages = "70-81",
year = {1999},
month = nov,
URL = ftpdir # {ovlinger-wand-99.ps},
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.},
source = {papers/oopsla-99/myfinal/preprint.tex}
}
@Article{Wand99a,
author = {Mitchell Wand},
title = {Continuation-Based Multiprocessing Revisited},
journal = {Higher-Order and Symbolic Computation},
year = 1999,
volume = 12,
number = 3,
month = oct,
pages = 283,
URL = ftpdir # {hosc-99-intro.ps},
abstract = {This is a short introduction to the republication of
"Continuation-Based Multiprocessing," which
originally appeared in the 1980 Lisp Conference.},
source = {papers/lfp-80/revised/intro.tex}
}
@Article{Wand99b,
author = {Mitchell Wand},
title = {Continuation-Based Multiprocessing},
journal = {Higher-Order and Symbolic Computation},
year = 1999,
volume = 12,
number = 3,
month = oct,
pages = {285-299},
note = {Originally appeared in the 1980 Lisp Conference},
URL = ftpdir # {hosc-99.ps},
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.},
source = {papers/lfp-80/revised/kmulti.tex}
}
@InProceedings{GanzFriedmanWand99,
author = {Steven E. Ganz and Daniel P. Friedman and Mitchell Wand},
title = {Trampolined Style},
booktitle = icfp99,
year = 1999,
address = {Paris},
month = sep,
pages = {18-27},
URL = ftpdir # {icfp-99.ps},
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.},
source = {~/papers/icfp-99}
}
#Unpublished{Sobeletal99,
author = {Jonathan Sobel and Steven E. Ganz and Daniel
P. Friedman and Mitchell Wand},
title = {A Monadic Categorical Semantics for Threads},
note = {unpublished note},
OPTkey = {},
year = {1999},
month = jul,
URL = ftpdir # {sobel-etal-99.ps},
abstract = {Rather than relegating threads to be a machine-level
concept, it is possible to describe thread semantics
at the programming-language level. Here, a
categorical semantics is given for a potentially
multithreaded programming language. The thread
behavior is packaged as a monad, and the semantics
is described both directly and via a
semantics-preserving ``trampolining'' translation
into a lambda-calculus-like metalanguage. The
semantics captures the notions of incremental work,
interleaving, and it supports language-level thread
operators. Different thread monads, their
properties, and the operators they support are
discussed.},
source = {~/papers/popl-00},
OPTannote = {}
}
@Book{FriedmanWandHaynes01,
author = "Daniel P. Friedman and Mitchell Wand and Christopher
T. Haynes",
title = "Essentials of Programming Languages",
edition = "Second",
publisher = "MIT Press",
year = "2001",
address = "Cambridge, MA",
URL = "http://www.cs.indiana.edu/eip/eopl.html",
}
@Article{WandClinger:JFP-01,
author = {Mitchell Wand and William D. Clinger},
title = {Set Constraints for Destructive Array Update Optimization},
journal = {Journal of Functional Programming},
volume = 11,
number = 3,
pages = {319-346},
month = may,
year = {2001},
URL = ftpdir # "jfp-01.ps",
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.
},
source = {~/papers/jfp-01},
}
@InProceedings{MeunierEtAl:SchemeWorskhop-01,
author = {Philippe Meunier and Robby Findler and Paul
A. Steckler and Mitchell Wand},
title = {Selectors Make Analyzing Case-Lambda Too Hard},
booktitle = {Proc. Scheme 2001 Workshop},
OPTcrossref = {},
OPTkey = {},
OPTeditor = {Manuel Serrano},
OPTvolume = {},
OPTnumber = {},
series = {Technical Report: Informatique, Signaux et Systemes de Sophia-Antipolis, I3S/RT-2001-12-FR},
year = {2001},
OPTorganization = {},
OPTpublisher = {},
OPTaddress = {},
month = sep,
pages = "54-64",
URL = ftpdir # {meunier-etal-01.ps},
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.},
source = {papers/scheme-01},
OPTannote = {}
}
@Article{ MeunierEtAl:HOSC-05,
author = {Philippe Meunier and Robby Findler and Paul
A. Steckler and Mitchell Wand},
title = {Selectors Make Analyzing Case-Lambda Too Hard},
journal = {Higher-Order and Symbolic Computation},
year = {2005},
OPTkey = {},
volume = {18},
number = {3-4},
pages = {245-269},
month = dec,
OPTnote = {},
OPTannote = {},
URL = ftpdir # {hosc-05.pdf},
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.},
source = {papers/scheme-01},
}
@InProceedings{Wand:SAIG01,
author = {Mitchell Wand},
title = {A Semantics for Advice and Dynamic Join Points in
Aspect-Oriented Programming},
booktitle = {Proceedings of SAIG '01},
OPTcrossref = {},
OPTkey = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
series = lncs,
year = {2001},
OPTorganization = {},
publisher = springer,
address = springeraddr,
month = sep,
OPTpages = {},
note = {invited talk},
URL = ftpdir # {saig-01.ps},
OPTabstract = {},
source = {papers/saig-01},
OPTannote = {}
}
#Misc{WandKiczalesDutchyn02,
OPTkey = {},
author = {Mitchell Wand and Gregor Kiczales and Christopher Dutchyn},
title = {A Semantics for Advice and Dynamic Join Points in
Aspect-Oriented Programming},
howpublished = {appeared in Informal Workshop Record of FOOL 9, pages 67-88; also presented at FOAL (Workshop on Foundations of Aspect-Oriented Languages), a satellite event of AOSD 2002},
year = {2002},
URL = ftpdir # {w-k-d-01.ps},
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.},
OPTsource = {},
OPTannote = {}
}
@Unpublished{WandLieber02,
OPTkey = {},
author = {Mitchell Wand and Karl Lieberherr},
title = {Navigating through Object Graphs Using Local
Meta-Information},
OPThowpublished = {Submitted for publication},
year = {2002},
month = jun,
note = {unpublished report},
URL = ftpdir # {navigation-02.ps},
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.} ,
source = {~/papers/navigation-02},
OPTannote = {}
}
#InProceedings{WandWilliamson02,
OPTkey = {},
author = {Mitchell Wand and Galen B. Williamson},
title = {A Modular, Extensible Proof Method for Small-step Flow Analyses},
year = {2002},
month = apr,
note = {to appear in ESOP 2002},
URL = ftpdir # {wand-williamson-01.ps},
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.},
source = {~/papers/esop-02},
OPTannote = {}
}
@InProceedings{WandWilliamson:ESOP-02,
author = {Mitchell Wand and Galen B. Williamson},
title = {A Modular, Extensible Proof Method for Small-step
Flow Analyses},
editor = {Daniel Le M{\'e}tayer},
booktitle = {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},
publisher = springer,
series = {Lecture Notes in Computer Science},
volume = {2305},
year = {2002},
address = springeraddr,
pages = {213-227},
URL = ftpdir # {wand-williamson-01.ps},
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.},
source = {~/papers/esop-02},
}
Unpublished{Wand02,
author = {Mitchell Wand},
title = {Analyses that Distinguish Different Evaluation Orders, or,
Unsoundness Results in Control-Flow Analysis},
note = {unpublished},
OPTkey = {},
year = {2002},
month = jul,
URL = ftpdir # {order-sensitive-cfa.ps},
abstract = {The standard control-flow analysis for higher-order
languages, 0CFA, as defined by Sestoft, Shivers, Palsberg,
et al., has been shown correct for a variety of semantics.
One view of this family of results is that it shows that 0CFA is
insensitive to evaluation order. We present simple modifications of
0CFA for call-by-value and call-by-name that distinguish
call-by-value, call-by-name, and unrestricted beta-reduction.},
source = {~/papers/order-sensitive-cfa-02},
OPTannote = {}
}
#Misc{WandKiczalesDutchyn02b,
OPTkey = {},
author = {Mitchell Wand and Gregor Kiczales and Christopher Dutchyn},
title = {A Semantics for Advice and Dynamic Join Points in
Aspect-Oriented Programming},
howpublished = {submitted for publication},
year = {2002},
URL = ftpdir # {wkd02.ps},
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.},
note = {expanded version of WandKiczalesDutchyn02.},
OPTsource = {},
OPTannote = {}
}
@Article{WandKiczalesDutchyn:TOPLAS-04,
author = {Mitchell Wand and Gregor Kiczales and Christopher Dutchyn
},
title = {A Semantics for Advice and Dynamic Join Points in
Aspect-Oriented Programming},
journal = {TOPLAS},
year = {2004},
OPTkey = {},
volume = {26},
number = {5},
month = {September},
pages = {890-910},
note = {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. },
URL = ftpdir # {wkd02.ps},
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.},
OPTsource = {},
OPTannote = {}
}
Replaced by Wand:Krivine07
#Unpublished{Wand:Krivine03,
author = {Mitchell Wand},
title = {On the Correctness of the Krivine Machine},
note = {to appear in HOSC Special Issue on the Krivine Machine (expected in 2008)},
OPTkey = {},
year = {2003},
month = oct,
URL = ftpdir # {wand-krivine-03.ps},
abstract = {We provide a short proof of the correctness of the
Krivine machine by showing how it simulates weak
head reduction.},
source = {~/papers/krivine-02},
OPTannote = {}
}
@Article{Wand:Krivine07,
author = {Mitchell Wand},
title = {On the Correctness of the Krivine Machine},
journal = hosc,
year = {2007},
volume = {20},
number = {3},
pages = {231-236},
month = sep,
URL = ftpdir # {wand-krivine-03.ps},
abstract = {We provide a short proof of the correctness of the
Krivine machine by showing how it simulates weak
head reduction.},
source = {~/papers/krivine-02},
}
#Unpublished{Wand03,
author = {Mitchell Wand},
title = {Putting Failure in Context: Abstract Data Types of
Computations and Contexts},
note = {submitted for publication},
OPTkey = {},
year = {2003},
month = mar,
URL = ftpdir # {wand-03.ps},
abstract = {There are two standard models of backtracking programs: a model in
which the many possible answers are represented as a stream, and a
model in which the action of the backtracking program is represented
by two continuations: a success continuation and a failure
continuation. These two models, both intuitively plausible, have
never been (to our knowledge) been formally related. We show how
the two-continuation model can be derived from the stream model.
We do this by treating computations and contexts as abstract data
types. We start by representing computations as elements in a term
algebra. We derive an operational semantics for this term algebra
by representing it in an extension of call-by-value PCF. This
allows us to build an algebra of contexts, in which the usual
representation of contexts as terms with holes is an initial
algebra. We then represent these contexts as a final algebra using
two observers, one representing the action of the context on
success, and one representing its action on failure. Finally, we
regain a compositional semantics by representing computations by
their action on contexts.
},
source = {papers/putting-failure-in-context-02-03},
annote = {This paper has many bugs, so I am taking it off my list.}
}
@InProceedings{ShiversWand:ESOP-05,
author = {Olin Shivers and Mitchell Wand},
title = {Bottom-up beta-reduction: uplinks and lambda-DAGs},
editor = {Mooly Sagiv},
booktitle = {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},
publisher = springer,
series = {Lecture Notes in Computer Science},
volume = {3444},
year = {2005},
address = springeraddr,
URL = ftpdir # {shivers-wand-05.pdf},
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},
source = {papers/shivers-betasub-03},
note = {expanded version available as BRICS Technical Report RS-04-38, Department of Computer Science, University of {\AA}rhus.}
}
#TechReport{Shivers-Wand:bubs-tr,
author = {Olin Shivers and Mitchell Wand},
title = {Bottom-up $\beta$-reduction: Uplinks and $\lambda$-{DAG}s
(extended version)},
type = {Research Series},
number = {RS-04-38},
institution = {BRICS},
address = {Department of Computer Science, University of {\AA}rhus},
month = dec,
year = 2004,
annote = {Recommended version of ESOP 2005 article.}
}
@InProceedings{Wand:ICFP-03,
author = {Mitchell Wand},
title = {Understanding Aspects (Extended Abstract)},
booktitle = icfp,
OPTcrossref = {},
OPTkey = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
year = {2003},
OPTorganization = {},
OPTpublisher = {},
OPTaddress = {},
month = aug,
OPTpages = {},
note = {Summary of invited talk to be given at ICFP 2003},
URL = ftpdir # {icfp-03.ps},
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.
},
OPTsource = {},
OPTannote = {}
}
@Article{PalsbergWand:JFP-03,
author = {Jens Palsberg and Mitchell Wand},
title = {CPS Transformation of Flow Information},
journal = {Journal of Functional Programming},
volume = 13,
number = 5,
year = {2003},
month = sep,
pages = {905-923},
URL = ftpdir # {jfp-03.pdf},
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. },
source = {~/papers/jfp-03},
annote = {previously listed as PalsbergWand00, from ~/papers/cps-flow-99. Based on work done around 1998, as I recall. },
}
#Unpublished{CliftonLeavensWand-03,
author = {Curtis Clifton and Gary T. Leavens and Mitchell Wand},
title = {Parameterized Aspect Calculus: A Core Calculus for
the Direct Study of Aspect-Oriented Languages},
note = {submitted for publication},
OPTkey = {},
year = {2003},
month = oct,
URL = ftpdir # {clw-03.pdf},
abstract = {Formal study of aspect-oriented languages is
difficult because current theoretical models provide
a range of features that is too limited and rely on
encodings using lower-level abstractions, which
involve a cumbersome level of indirection. We
present a calculus, based on Abadi and Cardelli's
object calculus, that explicitly odels a base
language and a variety of point cut description
languages. This explicit modeling makes clear the
aspect-oriented features of the calculus by removing
the indirection of some existing models. We
demonstrate the generality of our calculus by
presenting models for AspectJ's open classes and
advice, and HyperJ's compositions, and sketching a
model for DemeterJ's adaptive methods.},
source = {~/papers/clifton-03},
OPTannote = {rejected from AOSD 04}
}
#Unpublished{WandVaillancourt-04,
author = {Mitchell Wand and Dale Vaillancourt},
title = {Relating Models of Backtracking},
note = {ICFP, to appear},
OPTkey = {},
month = apr,
year = {2004},
OPTannote = {},
URL = ftpdir # {wand-vaillancourt-04.pdf},
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.},
source = {~/papers/icfp-04},
}
@InProceedings{WandVaillancourt:ICFP-04,
author = {Mitchell Wand and Dale Vaillancourt},
title = {Relating Models of Backtracking},
OPTcrossref = {},
OPTkey = {},
booktitle = icfp,
pages = {54--65},
year = {2004},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
URL = ftpdir # {icfp-04.pdf},
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.},
source = {~/papers/icfp-04},
OPTnote = {},
OPTannote = {}
}
@InProceedings{ KoutavasWand:POPL-06,
author = {Vasileios Koutavas and Mitchell Wand},
title = {Small Bisimulations for Reasoning About Higher-Order
Imperative Programs},
booktitle = popl06,
pages = {141-152},
month = jan,
year = {2006},
URL = ftpdir # {popl-06.pdf},
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.},
source = {papers/popl-06},
}
@InProceedings{ KoutavasWand:ESOP-06,
author = {Vasileios Koutavas and Mitchell Wand},
title = {Bisimulations for Untyped Imperative Objects},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proc. ESOP 2006},
pages = {146-161},
year = {2006},
editor = {Peter Sestoft},
volume = {3924},
OPTnumber = {},
series = lncs,
address = springeraddr,
month = mar,
OPTorganization = {},
publisher = springer,
OPTnote = {},
OPTannote = {},
source = {papers/esop-06},
URL = ftpdir # {esop-06.pdf},
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.},
}
#Unpublished{ KoutavasWand06,
author = {Vasileios Koutavas and Mitchell Wand},
title = {Proving Class Equivalence},
note = {submitted for publication},
OPTkey = {},
month = jul,
year = {2006},
OPTannote = {},
URL = ftpdir # {koutavas-wand-06.pdf},
abstract = {We present a sound and complete method for reasoning
about contextual equivalence between different
implementations of classes in an imperative subset of
Java. Our technique successfully deals with public and
private methods and fields, imperative fields,
inheritance, and invocations of callbacks. To the
extent of our knowledge this is the first sound and
complete proof method of equivalence between classes for
such a subset of Java. Using our technique we were able
to prove equivalences in examples with higher-order
behavior, where previous methods for functional calculi
admit limitations (e.g. [Pitts and Stark 1998, Sumii and
Pierce 2005]). We were also able to show equivalences
between classes that expose part of their state using
public fields, hide part of their functionality using
private methods, and are extensible by the surrounding
context. Other reasoning techniques for class-based
languages (e.g. Banerjee and Naumann 2005,Jeffrey and
Rathke 2005) restrict the way a class communicates with
and abstracts functionality from its context. We derive
our technique following a methodology similar to our
previous work on functional languages [Koutavas and
Wand, POPL 2006] and object-based languages [Koutavas
and Wand, ESOP 2006], thus showing that this methodology
gives useful results in a diversity of languages. },
}
@InProceedings{ Koutavas-Wand:FOOL-07,
author = {Vasileios Koutavas and Mitchell Wand},
title = {Reasoning About Class Behavior},
month = jan,
year = 2007,
booktitle = {Informal Workshop Record of FOOL 2007},
OPTpages = {},
OPTyear = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
URL = ftpdir # {koutavas-wand-06b.pdf},
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. }
}
#Unpublished{HermanWand07,
author = {David Herman and Mitchell Wand},
title = {A Theory of Hygienic Macros},
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.},
URL = ftpdir # {herman-wand-07.pdf},
note = {to appear in ESOP 2008},
OPTkey = {},
month = oct,
year = {2007},
OPTannote = {}
}
@InProceedings{ HermanWand-08,
author = {David Herman and Mitchell Wand},
title = {A Theory of Hygienic Macros},
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.},
URL = ftpdir # {herman-wand-07.pdf},
OPTcrossref = {},
OPTkey = {},
booktitle = {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.},
pages = {48-62},
year = {2008},
OPTeditor = {},
volume = {4960},
OPTnumber = {},
series = lncs,
address = springeraddr,
OPTmonth = {},
OPTorganization = {},
publisher = springer,
note = {http://dx.doi.org/10.1007/978-3-540-78739-6\_4},
OPTannote = {}
}
#Unpublished{VardoulakisWand07,
author = {Dimitris Vardoulakis and Mitchell Wand},
title = {A Compositional Trace Semantics for Orc},
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.},
note = {submitted for publication},
URL = ftpdir # {vardoulakis-wand-07.pdf},
OPTkey = {},
month = oct,
year = {2007},
OPTannote = {}
}
@InProceedings{ VardoulakisWand-08,
author = {Dimitris Vardoulakis and Mitchell Wand},
title = {A Compositional Trace Semantics for Orc},
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.},
OPTcrossref = {},
OPTkey = {},
booktitle = {Coordination Models and Languages: 10th International Conference, COORDINATION 2008, Oslo, Norway, June 4-6, 2008},
pages = {331-346},
year = {2008},
OPTeditor = {},
volume = {5052},
OPTnumber = {},
series = lncs,
address = springeraddr,
OPTmonth = {},
OPTorganization = {},
publisher = springer,
note = {http://dx.doi.org/10.1007/978-3-540-68265-3\_21},
URL = ftpdir # {vardoulakis-wand-07.pdf},
OPTannote = {}
}
@InProceedings{ DimoulasWand-09,
author = {Christos Dimoulas and Mitchell Wand},
title = {The Higher-Order Aggregate Update Problem},
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.},
URL = ftpdir # {wand-dimoulas-08.pdf},
source = {~/papers/vmcai-09},
booktitle = {Verification, Model Checking, and Abstract Interpretation, 10th International Conference},
pages = {44-58},
year = {2009},
editor = {Neil D. Jones and Markus Muller-Olm},
volume = {5403},
OPTnumber = {},
series = lncs,
address = springeraddr,
month = jan,
OPTorganization = {},
publisher = springer,
OPTnote = {},
OPTannote = {}
}
@Book{ FriedmanWand-08,
author = "Daniel P. Friedman and Mitchell Wand",
title = "Essentials of Programming Languages",
edition = "Third",
publisher = "MIT Press",
year = "2008",
address = "Cambridge, MA",
URL = "http://www.eopl3.com",
}
@Unpublished{TuronWand-09,
author = {Aaron Turon and Mitchell Wand},
title = {A Separation Logic for the Pi-calculus},
note = {unpublished},
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.},
URL = ftpdir # {turon-wand-09.pdf},
source = {~/papers/popl-10},
OPTkey = {},
month = jul,
year = {2009},
OPTannote = {}
}
@InProceedings{TuronWand:POPL-11,
author = {Aaron Turon and Mitchell Wand},
title = {A separation logic for refining concurrent objects},
booktitle = popl,
pages = {247-258},
URL = wwwdir # {turon-wand-10.pdf},
source = {~/papers/popl-11},
OPTkey = {},
month = jan,
year = {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.}
}
@Article{ShiversWand:BUBS-JournalVersion-10,
author = {Olin Shivers and Mitchell Wand},
title = {Bottom-up beta-reduction: uplinks and lambda-DAGs (journal version)},
journal = "Fundamenta Infomaticae",
year = {2010},
month = jul,
volume = "103",
number = "1-4",
pages = "247-287",
URL = wwwdir # {shivers-wand-10.pdf},
source = {~/papers/shivers-bubs-10},
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.},
OPTannote = {}
}
@InProceedings{StansiferWand:LDTA-11,
author = {Paul Stansifer and Mitchell Wand},
title = {Parsing Reflective Grammars},
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.},
OPTcrossref = {},
OPTkey = {},
booktitle = {Workshop on Language Descriptions, Tools, and
Applications (LDTA)},
pages = {73-79},
year = {2011},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
address = {Saarbrucken, Germany},
month = mar,
OPTorganization = {},
OPTpublisher = {},
note = {},
OPTannote = {},
source = {papers/ldta-11},
URL = {http://arxiv.org/abs/1102.2003}
}
@InProceedings{Turon-Wand:MFPS-2011,
author = {Aaron Turon and Mitchell Wand},
title = {A resource analysis of the pi-calculus},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings 27th Conf. on the Mathematical Foundations of Programming Semantics (MFPS)},
OPTpages = {},
year = {2011},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
series = {Electronic Notes in Computer Science},
OPTaddress = {},
month = may,
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
URL = {http://arxiv.org/abs/1105.0966},
source = {~/papers/mfps-11},
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.},
}
@InProceedings{Stansifer-Wand:ICFP-2014,
author = {Paul Stansifer and Mitchell Wand},
title = {Romeo: a system for more flexible binding-safe programming},
OPTcrossref = {},
OPTkey = {},
booktitle = icfp,
year = 2014,
pages = {53--65},
url = {http://doi.acm.org/10.1145/2628136.2628162},
doi = {10.1145/2628136.2628162},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTpages = {},
OPTmonth = {},
OPTaddress = {},
OPTorganization = {},
OPTpublisher = {},
source = {https://github.com/mwand/alpha-agnostic.git/icfp2014},
OPTannote = {},
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.}
}
@Article{Stansifer-Wand:JFP-2016,
author = {Paul Stansifer and Mitchell Wand},
title = {Romeo: a system for more flexible binding-safe programming},
journal = {Journal of Functional Programming},
year = {2016},
OPTkey = {},
volume = {26},
number = {e13},
doi = {10.1017/S0956796816000137},
url = {http://www.ccs.neu.edu/home/wand/papers/stansifer-wand-jfp-16.pdf},
OPTpages = {},
OPTmonth = {},
note = {doi: {10.1017/S0956796816000137}. Preliminary version appeared in ICFP 2014},
OPTannote = {},
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.}
}
@Article{Pombrio-Krishnamurthi-Wand:ICFP-2017,
author = {Justin Pombrio and
Shriram Krishnamurthi and
Mitchell Wand},
title = {Inferring scope through syntactic sugar},
journal = {PACMPL},
volume = {1},
number = {ICFP},
pages = {44:1--44:28},
year = {2017},
url = {http://doi.acm.org/10.1145/3110288},
doi = {10.1145/3110288},
timestamp = {Tue, 12 Sep 2017 16:16:51 +0200},
biburl = {https://dblp.org/rec/bib/journals/pacmpl/PombrioKW17},
bibsource = {dblp computer science bibliography, https://dblp.org},
OPTurl = wwwdir # {ifcp-2017.pdf},
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. }
}