@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{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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = "ftp://ftp.ccs.neu.edu/pub/people/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 = "ftp://ftp.ccs.neu.edu/pub/people/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 = "ftp://ftp.ccs.neu.edu/pub/people/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 = "ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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 = {ftp://ftp.ccs.neu.edu/pub/people/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

selectorsto 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) usesselectorsto 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.} } @Unpublished{ShiversWand:BUBS-JournalVersion-10, author = {Olin Shivers and Mitchell Wand}, title = {Bottom-up beta-reduction: uplinks and lambda-DAGs (journal version)}, journal = "Fundamenta Infomaticae", OPTyear = {}, OPTvolume = "", OPTnumber = "", OPTpages = "", note = {to appear}, 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.}, month = jul, year = {2010}, 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 = {}, note = {to appear}, 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.}, }