@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,
}

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,
  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 = {Proc. ACM Programming Languages}, year = {2017}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, pages = {28 pages}, OPTmonth = {}, note = {to appear in ICFP 2017}, OPTannote = {}, url = 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. } }