@preamble{
"\def\oldpopl#1{{\it {Conf. Rec. #1 ACM Symposium on Principles of
Programming Languages}\/}}
\def\popl#1{{\it {Proceedings #1 Annual 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{esop = "European Symposium on Programming"}
@string{gcse = "International Symposium on Generative and Component-Based Software Engineering"}
@string{ic = {Information and Computation}}
@string{lncs = "Lecture Notes in Computer Science"}
@string{popl = "Proceedings ACM Symposium on Principles of Programming Languages"}
@string{popl4 = "Proceedings 4th Annual ACM Symposium on Principles of
Programming Languages"}
@string{popl12 = "Conference Record of the 12th Annual ACM Symposium
on Principles of Programming Languages"}
@string{popl20 = "Proceedings 20th Annual ACM Symposium on Principles
of Programming
Languages"}
@string{popl21 = "Proceedings 21st Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl22 = "Proceedings 22nd Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl23 = "Proceedings 23rd Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl24 = "Proceedings 24th Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl25 = "Proceedings 25th Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl26 = "Proceedings 26th Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl27 = "Proceedings 27th Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl31 = "Proceedings 31st Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl32 = "Proceedings 32nd Annual ACM Symposium on Principles
of Programming Languages"}
@string{popl06 = "Proceedings 33rd ACM Symposium on Programming Languages"}
@string{springer = "Springer-Verlag"}
@string{springeraddr = "Berlin, Heidelberg, and New York"}
@string{lics89 = "Proc. 4th IEEE Symposium on Logic in Computer Science"}
@string{lics90 = "Proc. 5th IEEE Symposium on Logic in Computer Science"}
@string{lics02 = "Proc. 17th IEEE Symposium on Logic in Computer Science"}
@string{lics = "Proc. IEEE Symposium on Logic in Computer Science"}
@string{lfp90 = "Proc. 1990 ACM Symposium on Lisp and Functional Programming"}
@string{lfp86 = "Proc. 1986 ACM Symposium on Lisp and Functional Programming"}
@string{lfp88 = "Proc. 1988 ACM Symposium on Lisp and Functional Programming"}
@string{lfp94 = "Proc. 1994 ACM Symposium on Lisp and Functional Programming"}
@string{pldi95 = "Proc. ACM SIGPLAN '95 Conference on Programming
Language Design and Implementation"}
@string{pldi96 = "Proc. ACM SIGPLAN '96 Conference on Programming
Language Design and Implementation"}
@string{pldi97 = "Proc. ACM SIGPLAN '97 Conference on Programming
Language Design and Implementation"}
@string{pldi98 = "Proc. ACM SIGPLAN '98 Conference on Programming
Language Design and Implementation"}
@string{icfp99 = "Proc. 1999 ACM SIGPLAN International Conference on Functional Programming"}
@string{icfp00 = "Proc. 2000 ACM SIGPLAN International Conference on Functional Programming"}
@string{icfp03 = "Proc. 2003 ACM SIGPLAN International Conference on Functional Programming"}
@string{icfp = "Proc. ACM SIGPLAN International Conference on Functional Programming"}
@string{oopsla = "Proceedings {ACM} Conference on Object-Oriented
Programming Systems, Languages, and Applications"}
@string{ecoop = "Proceedings European Conference on Object-Oriented
Programming"}
@string{aosd = "Proc. International Conference on Aspect-Oriented
Software Development"}
@string{ftpdir = "ftp://ftp.ccs.neu.edu/pub/people/wand/papers/"}
@Article{ ACM68,
author = "{Association for Computing Machinery}",
title = "Curriculum 68--Recommendations for Academic Programs
in Computer Science -- A Report of the {ACM} Curriculum Committee on Computer Science",
journal = "Communications of the ACM",
year = "1968",
volume = "11",
pages = "151--197",
}
@article{ AOP:CACM2001,
author = {Tzilla Elrad and Robert E. Filman and Atef Bader},
title = {Aspect-oriented programming: Introduction},
journal = {Communications of the ACM},
volume = {44},
number = {10},
year = {2001},
issn = {0001-0782},
pages = {29--32},
doi = {http://doi.acm.org/10.1145/383845.383853},
publisher = {ACM Press},
}
@Unpublished{ AbadiCardelli93,
author = "Martin Abadi and Luca Cardelli",
title = "A Theory of Primitive Objects",
note = "draft",
year = "1993",
month = oct,
}
@Article{ AbadiCardelli96,
author = {Martin Abadi and Luca Cardelli},
title = {A Theory of Primitive Objects: Untyped and
First-Order Systems},
journal = ic,
year = 1996,
volume = 125,
number = 2,
month = mar,
pages = {78-102}
}
@Book{ AbadiCardelli:book96,
author = "Mart{\'{\i}}n Abadi and Luca Cardelli",
title = "A Theory of Objects",
publisher = springer,
address = springeraddr,
year = "1996",
ISBN = "0-387-94775-2",
}
@Article{ AbadiEtAl91,
author = "Mart\'{\i}n Abadi and Luca Cardelli and Pierre-Louis
Curien and Jean-Jacques L{\'e}vy",
title = "Explicit Substitutions",
journal = "Journal of Functional Programming",
volume = "1",
number = "4",
pages = "375--416",
year = "1991",
abstract = "The $\lambda$$\sigma$-calculus is a refinement of the
$\lambda$-calculus where substitutions are manipulated
explicitly. The $\lambda$$\sigma$-calculus provides a
setting for studying the theory of substitutions, with
pleasant mathematical properties. It is also a useful
bridge between the classical $\lambda$-calculus and
concrete implementations.",
note = "Summary in \bgroup\em {ACM} {S}ymposium on
{P}rinciples of {P}rogramming {L}anguages ({POPL}),
{S}an {F}rancisco, {C}alifornia\egroup, 1990",
}
@InProceedings{ AbadiLampsonLevy96,
author = "Abadi, Mart{\'{\i}}n and Lampson, Butler and L{\'{e}}vy, Jean-Jacques",
title = "Analysis and Caching of Dependencies",
booktitle = "Proceedings of the ACM '96 International Conference on
Functional Programming",
year = "1996",
pages = "83--91",
}
@Book{ AbelsonSussman84,
author = "Hal Abelson and Gerald Jay Sussman",
title = "The Structure and Interpretation of Computer Programs",
publisher = "MIT Press",
year = "1985",
address = "Cambridge, MA",
}
@InCollection{ Abramsky90,
author = "Samson Abramsky",
title = "The lazy lambda calculus",
pages = "65-116",
publisher = "Addison-Wesley",
year = "1990",
editor = "David A. Turner",
booktitle = "Research Topics in Functional Programming",
OPTvolume = "",
OPTseries = "",
OPTaddress = "",
OPTedition = "",
OPTmonth = "",
OPTnote = ""
}
@Book{ AbramskyHankin87,
author = "Samson Abramsky and Christopher Hankin",
title = "Abstract Interpretation of Declarative Languages",
publisher = "John Wiley",
year = "1987",
address = "New York",
}
@inproceedings{ AbramskyHondaMcCusker-lics98,
author = {Samson Abramsky and
Kohei Honda and
Guy McCusker},
title = {A Fully Abstract Game Semantics for General References.},
booktitle = {LICS},
year = {1998},
pages = {334-344},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{ AbramskyJagadeesanMalacaria:ic00,
author = {Samson Abramsky and Radha Jagadeesan and Pasquale Malacaria},
title = {Full abstraction for {PCF}},
journal = {Inf. Comput.},
volume = {163},
number = {2},
year = {2000},
issn = {0890-5401},
pages = {409--470},
doi = {http://dx.doi.org/10.1006/inco.2000.2930},
publisher = {Academic Press, Inc.},
address = {Duluth, MN, USA},
note = {Originally appeared as \cite{AbramskyJagadeesanMalacaria:tacs94}}
}
@inproceedings{ AbramskyJagadeesanMalacaria:tacs94,
author = "Samson Abramsky and Pasquale Malacaria and Radha Jagadeesan",
title = "Full Abstraction for {PCF}",
booktitle = "Theoretical Aspects of Computer Software",
pages = "1-15",
year = "1994",
url = "citeseer.csail.mit.edu/article/abramsky96full.html" }
@article{ AbramskyOng93,
author = {Samson Abramsky and C.-H. Luke Ong},
title = {Full abstraction in the lazy lambda calculus},
journal = {Inf. Comput.},
volume = {105},
number = {2},
year = {1993},
issn = {0890-5401},
pages = {159--267},
doi = {http://dx.doi.org/10.1006/inco.1993.1044},
publisher = {Academic Press, Inc.},
address = {Duluth, MN, USA},
}
@Article{ Ackermann28,
author = "Ackermann, F. W.",
title = "Zum Hilbertschen Aufban d. Reelen Zahlen",
journal = "Mathematische Annalen",
year = "1928",
volume = "93",
pages = "118--133",
}
@InProceedings{ AgerEtAl:PPDP03,
author = "Mads Sig Ager and Dariusz Biernacki and
Olivier Danvy and Jan Midtgaard",
title = "A Functional Correspondence
between Evaluators and Abstract Machines",
year = "2003",
booktitle = "Proceedings of the Fifth ACM-SIGPLAN
International Conference on
Principles and Practice of Declarative Programming",
publisher = "ACM Press",
location = "Uppsala, Sweden",
pages = "8-19"
}
@Book{ AhoSethiUllman86,
author = "Aho, Alfred V. and Sethi, Ravi and Ullman, Jeffrey D.",
title = "Compilers: Principles, Techniques, and Tools",
publisher = "Addison-Wesley",
year = "1986",
address = "Reading, MA",
}
@INPROCEEDINGS{ AikenFahndrichLevien95,
AUTHOR = {A. Aiken and M. F\"{a}hndrich and R. Levien},
TITLE = "Better Static Memory Management: Improving
Region-Based Analysis of Higher-Order Languages",
BOOKTITLE = "1995 Conference on Programming Language Design
and Implementation" ,
ADDRESS = {San Diego, California},
MONTH = jun,
YEAR = 1995,
pages = {174-185},
}
@InProceedings{ Aksit:ecoop93,
author = "Mehmet Aksit and Ken Wakita and Jan Bosch and Lodewijk
Bergmans and Akinori Yonezawa",
editor = "Rachid Guerraoui and Oscar Nierstrasz and Michel
Riveill",
title = "{Abstracting Object Interactions Using Composition
Filters}",
booktitle = "Proceedings of the ECOOP'93 Workshop on Object-Based
Distributed Programming",
series = "LNCS 791",
pages = "152--184",
publisher = "Springer-Verlag",
address = springeraddr,
year = "1994",
keywords = "olit-obc obdp93 binder",
abstract = "It is generally claimed that object-based models are
very suitable for building distributed system
architectures since object interactions follow the
client-server model. To cope with the complexity of
today's distributed systems, however, we think that
high-level linguistic mechanisms are needed to
effectively structure, abstract and reuse object
interactions. For example, the conventional
object-oriented model does not provide high-level
language mechanisms to model layered system
architectures. Moreover, we consider the message
passing model of the conventional object-oriented model
as being too low-level because it can only specify
object interactions that involve two partner objects at
a time and its semantics cannot be extended easily.
This paper introduces Abstract Communication Types
(ACTs), which are objects that abstract interactions
among objects. ACT s make it easier to model layered
communication architectures, to enforce the invariant
behavior among objects, to reduce the complexity of
programs by hiding the interaction details in separate
modules and to improve reusability through the
application of object-oriented principles to ACT
classes. We illustrate the concept of ACT s using the
composition filters model."
}
@Book{ Allen78,
author = "Allen, John R.",
title = "Anatomy of LISP",
publisher = "McGraw-Hill",
year = "1978",
address = "New York",
}
@techreport{ AllenEtAl:tr05fortress,
author = {Eric Allen and David Chase and Victor Luchango and Jan-Willem Maessen and Sukyoung Ryu and Guy L. Steele, Jr. and Sam Tobin-Hochstadt},
title = "The {F}ortress Language Specification, version 0.618",
institution = "Sun Microsystems, Inc.",
year = {2005},
url = "http://research.sun.com/projects/plrg/fortress0618.pdf",
}
@Article{ Allison83,
author = "Allison, L.",
title = "Programming Denotational Semantics",
journal = "Computer Journal",
year = "1983",
volume = "26",
number = "2",
pages = "164--174",
}
@InProceedings{ AmadioCardelli,
author = "Amadio, Robert M. and Cardelli, Luca",
title = "Subtyping Recursive Types",
year = "1991",
pages = "104--118",
booktitle = "{\popl{18th}}",
}
@InProceedings{ Amtoft93,
author = "Torben Amtoft",
title = "Minimal Thunkification",
booktitle = "WSA '93",
year = 1993,
pages = "218--229",
publisher = springer,
series = lncs,
volume = 724,
address = springeraddr,
}
James H. Andrews, "Process-Algebraic Foundations of Aspect-Oriented Programming" Proceedings of the Third
International Conference on Metalevel Architectures and Separation of Crosscutting Concerns (Reflection 2001), Kyoto,
Japan, September 26-28, 2001. To appear in Springer LNCS. Copyright Springer-Verlag.
@InProceedings{ Andrews01,
author = {James H. Andrews},
title = {Process-Algebraic Foundations of Aspect-Oriented
Programming},
booktitle = {Proceedings of the Third International Conference
on Metalevel Architectures and Separation of
Crosscutting Concerns (Reflection 2001)},
volume = 2192,
series = lncs,
year = 2001,
publisher = springer,
address = springeraddr,
month = sep,
pages = {187-209}
}
@Book{ AndrewsOlsson93,
author = "G. R. Andrews and R. A. Olsson",
title = "The SR Programming Language: Concurrency in Practice",
publisher = "Benjamin/Cummings",
year = 1993,
address = "Redwood City, CA"
}
@Article{ Appel89,
author = "Appel, Andrew W.",
title = "Runtime Tags Aren't Necessary",
journal = "Lisp and Symbolic Computation",
year = "1989",
volume = "2",
pages = "153--162",
}
@Book{ Appel92,
author = "A. W. Appel",
title = "Compiling with Continuations.",
pages = "272",
publisher = "Cambridge University Press",
year = "1992",
}
@Book{ Appel98,
author = "Andrew W. Appel",
title = "Modern Compiler Implementation in ML",
publisher = "Cambridge University Press",
year = 1998,
address = "Cambridge, UK",
}
@InProceedings{ AppelJim89,
author = "Appel, Andrew W. and Jim, Trevor",
title = "Continuation-Passing, Closure-Passing Style",
year = "1989",
pages = "293--302",
booktitle = "{\popl{16th}}",
}
@TechReport{ AptMeertens77,
author = "Apt, Krzysztof R. and Meertens, L. G. L. T.",
title = "Completeness with Finite Systems of Intermedi\-ate
Assertions for Recursive Program Schemes",
institution = "Mathematisch Centrum",
year = "1977",
number = "IW84/77",
address = "Amsterdam",
month = "September",
}
@Book{ ArbibManes74,
author = "Arbib, Michael A. and Manes, Ernest G.",
title = "The Categorical Imperative",
publisher = "Academic Press",
year = "1974",
}
@Article{ ArbibManes78,
author = "Arbib, Michael A. and Manes, Ernest G.",
title = "Functorial Iteration Principle",
journal = "Notices of the American Mathematical Society",
year = "1978",
volume = "25",
pages = "A-381",
month = apr,
}
@Article{ ArbibManes80,
author = "Arbib, Michael A. and Manes, Ernest G.",
title = "Partially Additive Categories and Flow-Diagram Semantics",
journal = "Journal of Algebra",
year = "1980",
volume = "62",
pages = "203--227",
}
@Article{ ArbibManes82,
author = "Arbib, Michael A. and Manes, Ernest G.",
title = "The Pattern-of-Calls Expansion is the Canonical Fixpoint for Recursive Definitions",
journal = "Journal of the ACM",
year = "1982",
volume = "29",
pages = "577--602",
}
@Book{ ArnoldGosling:JavaLang,
author = "Ken Arnold and James Gosling",
key = "Arnold \& Gosling",
title = "The {Java} Programming Language",
publisher = "Ad{\-d}i{\-s}on-Wes{\-l}ey",
address = "Reading, MA",
year = "1998",
edition = "Second",
series = "The Java Series",
url = "http://www.aw.com/cp/javaseries.html",
}
@TechReport{ ArnoldNivat77,
author = "Arnold, A. and Nivat, Maurice",
title = "Non-deterministic Recursive Program Schemes",
institution = "IRIA",
type = "Research Report",
year = "1977",
number = "262",
month = nov
}
@Article{ AshcroftWadge76,
author = "Ashcroft, E. A. and Wadge, W. W.",
title = "Lucid, a formal system for writing and proving programs",
journal = "SIAM Journal on Computing",
year = "1976",
volume = "5",
pages = "336--354",
month = sep
}
@InProceedings{ AtkinsonHewitt77,
author = "Atkinson, Russell and Hewitt, Carl",
title = "Synchronization in Actor Systems",
year = "1977",
pages = "267--280",
booktitle = "{\popl{4th}}",
}
@InProceedings{ Aubin75,
author = "Aubin, R.",
title = "Some Generalization Heuristics in Proofs by Induction",
year = "1975",
pages = "197--208",
booktitle = "Proceedings IRIA Symposium on Proving and Improving Programs",
address = "Arc-et-Senans, France",
}
@Article{ AuslanderStrong78,
author = "Auslander, M. A. and Strong, H. R.",
title = "Systematic Recursion Removal",
journal = "Communications of the ACM",
year = "1978",
volume = "21",
pages = "127--133",
}
==== B ===
@inproceedings{ BachrachPlayford01:JSE,
author = {Jonthan Bachrach and Keith Playford},
title = {The {J}ava syntactic extender ({JSE})},
booktitle = oopsla,
year = {2001},
isbn = {1-58113-335-9},
pages = {31--42},
location = {Tampa Bay, FL, USA},
doi = {http://doi.acm.org/10.1145/504282.504285},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@InProceedings{ Backus73,
author = "Backus, John W.",
title = "Programming Language Semantics and Closed Applicative Languages",
year = "1973",
pages = "71--86",
booktitle = popl,
address = "Boston",
}
@Book{ BaetenWeijland90,
author = "J. C. M. Baeten and W. P. Weijland",
title = "Process Algebra",
publisher = "Cambridge University Press",
year = "1990",
OPTeditor = "",
OPTvolume = "",
OPTseries = "",
OPTaddress = "",
OPTedition = "",
OPTmonth = "",
OPTnote = ""
}
@InProceedings{ Baker72,
author = "Baker, F. T.",
title = "System Quality Through Structured Programming",
year = "1972",
pages = "339--343",
booktitle = "Proceedings Fall Joint Com\-pu\-ter Conference",
}
@Article{ Baker77,
author = "Baker, Jr., Henry G.",
title = "List Processing in Real Time on a Serial Computer",
journal = "Communications of the ACM",
note = "Originally appeared as MIT Artificial Intelligence
Laboratory Working Paper No. 39, February 1977"
}
@inproceedings{ BakerHsieh02:maya,
author = {Jason Baker and Wilson C. Hsieh},
title = {Maya: multiple-dispatch syntax extension in {J}ava},
booktitle = {PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation},
year = {2002},
isbn = {1-58113-463-0},
pages = {270--281},
location = {Berlin, Germany},
doi = {http://doi.acm.org/10.1145/512529.512562},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@article{ BanerjeeNaumann-jacm05,
author = {Anindya Banerjee and David A. Naumann},
title = {Ownership confinement ensures representation independence for object-oriented programs},
journal = {J. ACM},
volume = {52},
number = {6},
year = {2005},
issn = {0004-5411},
pages = {894--960},
doi = {http://doi.acm.org/10.1145/1101821.1101824},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@Article{ BarbutiMartelli83,
author = "Barbuti, R. and Martelli, A.",
title = "A Structured Approach to Static Semantics Correctness",
journal = "Science of Computer Programming",
year = "1983",
volume = "3",
pages = "279--312",
}
@InCollection{ Barendregt77,
author = "Barendregt, Henk P.",
title = "The Type Free Lambda Calculus",
booktitle = "Handbook of Mathematical Logic",
year = "1977",
editor = "J.~Barwise",
pages = "1091--1132",
address = "Amsterdam",
publisher = "North-Holland",
}
@Book{ Barendregt81,
author = "Barendregt, Henk P.",
title = "The Lambda Calculus: Its Syntax and Semantics",
year = "1981",
address = "Am\-ster\-dam",
publisher = "North-Holland",
}
@Article{ Barendregt84,
author = "Barendregt, Henk P.",
title = "Introduction to Lambda Calculus",
journal = "Nieuw Archief voor Wiskunde",
year = "1984",
volume = "4",
number = "2",
pages = "337--372",
}
@Article{ Barendregt91,
author = "Henk Barendregt",
title = "Self-Interpretation in Lambda Calculus",
journal = "Journal of Functional Programming",
year = "1991",
volume = "1",
number = "2",
pages = "229-234",
month = apr,
}
@Book{ BarrettCouch79,
author = "Barrett, W. A. and Couch, J. D.",
title = "Compiler Construction: Theory and Practice",
publisher = "Science Research Associates",
year = "1979",
address = "Palo Alto, CA",
}
@inproceedings{ Batory98:JTS,
author = {D. Batory and B. Lofaso and Y. Smaragdakis},
title = {{JTS}: Tools for Implementing Domain-Specific Languages},
booktitle = {ICSR '98: Proceedings of the 5th International Conference on Software Reuse},
year = {1998},
isbn = {0-8186-8377-5},
pages = {143},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
}
@inproceedings{ BeckGamma98jUnit,
author="Kent Beck and Erich Gamma",
title="Test infected: Programmers love writing tests",
booktitle="Java Report",
volume=3,
issue=7,
pages="37--50",
year=1998
}
@Article{ Benabou68,
author = "Benabou, J.",
title = "Structures Algebriques dans les Cat\'egories",
journal = "Cahiers de Topologie et G\'eo\-m\'etrie Diff\'erentielle",
year = "1968",
volume = "10",
number = "1",
pages = "1--126",
}
@InProceedings{ BentonHughesMoggi:appsem2000,
author = {Nick Benton and John Hughes and Eugenio Moggi},
title = {Monads and Effects},
OPTcrossref = {},
OPTkey = {},
booktitle = {APPSEM},
pages = {42-122},
year = {2000},
editor = {Gilles Barthe and
Peter Dybjer and
Luis Pinto and
Jo{\~a}o Saraiva},
volume = {2395},
OPTnumber = {},
series = {Lecture Notes in Computer Science},
address = springeraddr,
OPTmonth = {},
OPTorganization = {},
OPTpublisher = springer,
OPTnote = {},
OPTannote = {}
}
@inproceedings{ BentonLeperchey05,
author = {Nick Benton and
Benjamin Leperchey},
title = {Relational Reasoning in a Nominal Semantics for Storage.},
booktitle = {Typed Lambda Calculi and Applications, 7th International
Conference, TLCA 2005, Nara, Japan, April 21-23, 2005,
Proceedings},
year = {2005},
pages = {86-101},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3461},
ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3461{\&}spage=86},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@Book{ Berge71,
author = "Berge, C.",
title = "Principles of Combinatorics",
publisher = "Academic Press",
year = "1971",
address = "New York",
}
@Inproceedings{ BergerHondaYoshida:icfp05,
author = {Martin Berger and Kohei Honda and Nobuko Yoshida},
title = {A Logical Analysis of Aliasing in Imperative
Higher-Order Functions},
booktitle = {Proceedings of the Tenth {ACM} {SIGPLAN}
International Conference on Functional Programming
({ICFP}`05)},
month = sep,
publisher = {ACM Press},
year = {2005},
notes = {To appear},
URL = {http://www.dcs.qmul.ac.uk/%7Ekohei/logics/imperative2short.ps}
}
@article{ Bergmans-Aksits:CACM2001,
author = {Lodewijk Bergmans and Mehmet Aksits},
title = {Composing crosscutting concerns using composition filters},
journal = {Communications of the ACM},
volume = {44},
number = {10},
year = {2001},
issn = {0001-0782},
pages = {51--57},
doi = {http://doi.acm.org/10.1145/383845.383857},
publisher = {ACM Press},
}
@Article{ Berry76,
author = "Berry, Gerard",
title = "Bottom-up Computation of Recursive Programs",
journal = "Revue Francaise d'Automa\-tique Informatique Recherche Operationelle",
year = "1976",
volume = "10",
number = "3",
pages = "47--82",
month = mar
}
@Article{ BerryCurien82,
author = "Berry, Gerard and Curien, Pierre-Louis",
title = "Sequential Algorithms on Concrete Data Structures",
journal = "Theoretical Computer Science",
year = "1982",
volume = "20",
pages = "265--321",
}
@techreport{ BiermanParkinsonPitts:tr03mj,
author = {Gavin Bierman and Matthew Parkinson and Andrew Pitts},
title = {{MJ}: {A}n imperative core calculus for {J}ava and {J}ava with Effects},
institution = {Cambridge University Computer Laboratory},
year = {2003},
number = {563},
month = {April},
url = {citeseer.ist.psu.edu/article/bierman03mj.html} }
@article{ BirkedalEtAl-lics05,
author = {Lars Birkedal and Noah Torp-Smith and Hongseok Yang},
title = {Semantics of Separation-Logic Typing and Higher-Order Frame Rules},
journal = lics,
year = {2005},
issn = {1043-6871},
pages = {260-269},
doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2005.47},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
@Book{ Birkhoff67,
author = "Birkhoff, Garrett",
title = "Lattice Theory",
publisher = "American Mathematical Society",
year = "1967",
address = "Providence, RI",
edition = "Third",
}
@Article{ BirkhoffLipson70,
author = "Birkhoff, G. and Lipson, D.",
title = "Heterogeneous Algebras",
journal = "Journal of Combinatorial Theory",
year = "1970",
volume = "8",
pages = "115--133",
}
@Book{ BirtwistleEtAl79,
author = "Birtwistle, G. M. and Dahl, O. J. and Myhrhaug, B. and Nygaard, K.",
title = "Simula Begin",
publisher = "Studentlitteratur",
year = "1979",
address = "Box 1717, S-221 01 Lund, Sweden",
}
@Book{ BjornerJones78,
title = "The Vienna Development Method: The Meta-Language",
publisher = Springer,
year = "1978",
editor = "Bjorner, Dines and Jones, Christopher B.",
volume = "61",
series = "Springer Lecture Notes in Computer Science",
address = "Berlin, Heidelberg, New York",
}
@InProceedings{ Bloom94,
author = "Bard Bloom",
title = "CHOCOLATE: Calculi of Higher Order COmmunication and
LAmbda TErms",
booktitle = "\popl{21st}",
year = "1994",
OPTeditor = "",
pages = "339-347",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
}
@Article{ BloomElgot76,
author = "Bloom, Steven L. and Elgot, Calvin C.",
title = "The Existence and Construction of Free Iterative Theories",
journal = "Journal of Computer and Systems Science",
year = "1976",
volume = "12",
pages = "305--318",
}
@InProceedings{ Bobrow86,
author = "D. G. Bobrow and K. Kahn and G. Kiczales and L.
Masinter and M. Stefik and F. Zdybel",
title = "{CommonLoops:} Merging {Common Lisp} and Object-Oriented
Programming",
booktitle = oopsla,
publisher = "ACM Press",
address = "New York",
month = oct,
year = "1986",
pages = "17--29",
}
@Article{ BobrowRaphael74,
author = "Daniel G. Bobrow and Bertram Raphael",
title = "New Programming Languages for Artificial Intelligence Research",
journal = "Computing Surveys",
year = "1974",
volume = "6",
pages = "155--174",
}
@Article{ BobrowWegbreit73,
author = "Daniel G. Bobrow and Ben Wegbreit",
title = "A Model and Stack Implementation of Multiple Environ\-ments",
journal = "Communications of the ACM",
year = "1973",
volume = "16",
pages = "591--602",
}
@InProceedings{ BodikGupta97,
author = "Bod{\'{\i}}k, Rastislav and Gupta, Rajiv",
title = "Partial Dead Code Elimination using Slicing Transformations",
booktitle = "Proceedings of the ACM SIGPLAN '97 Conference on
Programming Language Design and Implementation",
year = "1985",
pages = "7--21",
}
@InProceedings{ Bodwin82,
author = "Bodwin, J. and Bradley, L. and Kanda, J. and Little, D. and Pleban, U.",
title = "Experience with an Experimental Compiler Compiler Based on Denotational Semantics",
booktitle = "Proceedings of the SIGPLAN '82 Symposium on Compiler
Construction",
year = 1982,
pages = "216--229",
month = jun,
note = "{\it SIGPLAN Notices}, 17(6)"
}
@TechReport{ Bolek91,
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 = ""
}
@InProceedings{ Bowenetal93,
author = "Jonathan Bowen and Martin Franzle and Ernst-Rudiger Olderog
and Anders P. Ravn",
title = "Developing Correct Systems",
booktitle = "Proceedings of the 5th Euromicro Workshop on Real-Time Systems",
year = "1993",
publisher = "IEEE Computer Society Press",
}
@InCollection{ BoyerMoore72,
author = "Boyer, Robert S. and Moore, J. S.",
title = "The Sharing of Structure in Theorem-Proving Programs",
booktitle = "Machine Intelligence 7",
publisher = "Edinburgh University Press",
year = "1972",
editor = "B. Meltzer and D. Michie",
pages = "101--116",
}
@Article{ BoyerMoore77,
author = "Boyer, Robert S. and Moore, J. S.",
title = "A Lemma-Driven Automatic Theorem Prover for Recursive Function Theory",
journal = "Proceedings 5th International Joint Conference on
Artificial Intelligence",
year = "1977",
pages = "511--519",
}
@Book{ BoyerMoore79,
author = "Boyer, Robert S. and Moore, J. S.",
title = "A Computational Logic",
publisher = "Academic Press",
year = "1979",
address = "New York",
}
@inproceedings{ BrabandSchwartzbach:pepm02,
author = {Claus Brabrand and Michael I. Schwartzbach},
title = {Growing languages with metamorphic syntax macros},
booktitle = {PEPM '02: Proceedings of the 2002 ACM SIGPLAN Workshop on Partial evaluation and semantics-based program manipulation},
year = {2002},
isbn = {1-58113-455-X},
pages = {31--40},
location = {Portland, Oregon},
doi = {http://doi.acm.org/10.1145/503032.503035},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@Book{ BraffortHirschberg63,
editor = "P. Braffort and D. Hirschberg",
title = "Computer Programming and Formal Systems",
publisher = "North-Holland",
address = "Amsterdam",
year = "1963",
descriptor = "Automatentheorie, Kontextfrei, Logik, Mathematik,
Programmierung, Sprache",
}
@Book{ BrainerdLandweber74,
author = "Brainerd, W. S. and Landweber, L. H.",
title = "Theory of Computation",
publisher = "Wiley-Intersci\-ence",
year = "1974",
address = "New York",
}
@InProceedings{ BreazuTannenCoquandGunterScedrov89,
author = "Breazu-Tannen, Val and Coquand, Thierry and Gunter, Carl A. and Scedrov, Andre",
title = "Inheritance and Explicit Coercion: Preliminary Report",
booktitle = "{\lics{4th}}",
year = "1989",
pages = "112--129",
}
@Book{ BrinchHansen73,
author = "Brinch Hansen, Per",
title = "Operating Systems Principles",
publisher = "Prentice-Hall",
year = "1973",
address = "Englewood Cliffs, NJ",
}
@Article{ BrinchHansen75,
author = "Brinch Hansen, Per",
title = "The Programming Language {Concurrent} {PASCAL}",
journal = "IEEE Transactions on Software Engineering",
year = "1975",
volume = "SE-1",
pages = "199--207",
}
@Book{ BrinchHansen77,
author = "Brinch Hansen, Per",
title = "The Architecture of Concurrent Programs",
publisher = "Pren\-tice-Hall",
year = "1977",
address = "Englewood Cliffs, NJ",
}
@Article{ BrinchHansen78,
author = "Brinch Hansen, Per",
title = "Distributed Processes: A Concurrent Programming Concept",
journal = "Communications of the ACM",
year = "1978",
volume = "21",
pages = "934--941",
}
@InProceedings{ Brosgol80,
author = "Brosgol, B. M.",
title = "{$TCOL_{Ada}$} and the `Middle End' of the PQCC
Ada Compiler",
booktitle = "Proceedings ACM-SIGPLAN Symposium on the ADA Programming
Languages",
year = "1980",
pages = "101--112",
month = nov,
note = "SIGPLAN Notices, 15(11)"
}
@Article{ BroyWirsingPepper87,
author = "Broy, M. and Wirsing, M. and Pepper, P.",
title = "On the Algebraic Definition of Programming Languages",
journal = "ACM Transactions on Programming Languages and Systems",
year = "1987",
volume = "9",
pages = "54--99",
}
@Article{ BruceMeyerMitchell90,
author = "Bruce, Kim B. and Meyer, Albert R. and Mitchell, John C.",
title = "The Semantics of the Second-Order Lambda Calculus",
journal = "Information and Computation",
year = "1990",
volume = "85",
pages = "76--134",
}
@Article{ BrunoSethi76,
author = "Bruno, J. and Sethi, Ravi",
title = "Code Generation for a One-Register Machine",
journal = "Journal of the ACM",
year = "1976",
volume = "23",
pages = "502--510",
}
@InProceedings{ BrunsEtAl:concur2004,
author = {G. Bruns and R. Jagadeesan and A. S. A. Jeffrey and J. Riely},
title = {{muABC}: A Minimal Aspect Calculus},
booktitle = {Proc. Concur},
year = "2004",
pages = "209--224",
publisher = "Springer-Verlag",
volume = "3170",
series = "Lecture Notes in Computer Science",
url = {http://cm.bell-labs.com/who/ajeffrey/papers/concur04.pdf}
}
@inproceedings{ BrunsEtAl:concur2004tr,
author = "G. Bruns and R. Jagadeesan and A. Jeffrey and J. Riely",
title = "ABC: A minimal aspect calculus",
text = "G. Bruns, R. Jagadeesan, A. Jeffrey, and J. Riely. ABC: A minimal aspect
calculus. Full version, available at http://fpl.cs.depaul.edu/ajeffrey/papers/muABCfull.pdf,
2004.",
year = "2004",
url = "citeseer.ist.psu.edu/bruns04abc.html" }
@inproceedings{ BryantEtal:aosd02elide,
author = "Avi Bryant and Andrew Catton and Kris De Volder and Gail C. Murphy",
title = "Explicit Programming: Improving the Design Vocabulary of
Your Program",
booktitle="Proceedings of 1st International Conference on Aspect-Oriented Software Development",
month="April",
year=2002,
pages="10--18",
url = "citeseer.nj.nec.com/459253.html"
}
@Misc{ BuchiWright60,
author = "Buchi, J. R. and Wright, Jesse B.",
title = "Mathematical Theory of Automata",
howpublished = "course notes, Commu\-ni\-cation Sciences 403, University of Michigan",
year = "1960",
month = "Fall",
}
@Book{ Burge75,
author = "Burge, William H.",
title = "Recursive Programming Techniques",
publisher = "Addison-Wesley",
year = "1975",
address = "Reading, MA",
}
@TechReport{ Burge76,
author = "Burge, William H.",
title = "An Optimizing Technique for High Level Programming Languages",
institution = "IBM",
year = "1976",
type = "Research Report",
number = "RC-5834",
}
@Article{ BurnHankinAbramsky86,
author = "Burn, G. L. and Hankin, C. and Abramsky, S.",
title = "Strictness analysis for higher-order functions",
journal = "Science of Computer Programming",
volume = "7",
pages = "249--278",
year = 1986}
@Article{ Burstall69,
author = "Burstall, Rod M.",
title = "Proving Properties of Programs by Structural Induction",
journal = "Computer Journal",
year = "1969",
volume = "12",
number = "1",
pages = "41--48",
month = feb,
}
@InProceedings{ BurstallDarlington75,
author = "Burstall, Rod M. and Darlington, John",
title = "Some Transformations for Developing Recursive Pro\-grams",
booktitle = "Proceedings - 1975 International Conference on Reliable Software",
year = "1975",
pages = "465--472",
address = "Los Angeles",
}
@Article{ BurstallDarlington77,
author = "Burstall, Rod M. and Darlington, John",
title = "A Transformation System for Developing Recursive Programs",
journal = "Journal of the ACM",
year = "1977",
volume = "24",
pages = "44--67",
}
@InProceedings{ BurstallGoguen77,
author = "Burstall, Rod M. and Goguen, Joseph A.",
title = "Putting Theories Together to Make Specifications",
booktitle = "Proceedings 5th International Joint Conference on
Artificial Intelligence",
year = "1977",
pages = "1045--1058",
}
@InCollection{ BurstallLandin69,
author = "Burstall, Rod M. and Landin, Peter J.",
title = "Programs and their Proofs: An Algebraic Approach",
booktitle = "Machine Intelligence 4",
publisher = "American Elsevier",
year = "1969",
editor = "B. Meltzer and D. Michie",
pages = "17--44",
address = "New York",
}
@InProceedings{ BurstallMacQueenSannella80,
author = "Burstall, Rod M. and MacQueen, David B. and Sannella, Donald T.",
title = "HOPE: An Experimental Applicative Language",
booktitle = "Conference Record of the 1980 LISP Conference",
year = 1980,
pages = "136--143",
}
@InCollection{ Cadiou76,
author = "J. M. Cadiou",
title = "On Semantic Issues in the Relational Model of
Data",
booktitle = {\mfcs{1976}},
editor = "Mazurkiewicz",
year = "1976",
series = lncs,
publisher = Springer,
volume = "45",
pages = "23--38",
address = "Berlin, Heidelberg, New York",
}
@Article{ Cann92,
author = "David Cann",
title = "Retire {F}ortran? A Debate Rekindled",
journal = "Communications of the ACM",
month = "August",
year = "1992",
volume = "35",
number = "8",
pages = "81--89"
}
@InProceedings{ CanningEtAl89,
author = "Canning, Peter and Cook, William and Hill, Walter and Olthoff, W.",
title = "Interfaces for Strongly-Typed Object-Oriented Programming",
booktitle = "Proceedings 3rd Symposium on Object-Oriented Programming, Languages, and Systems",
year = "1989",
}
@Book{ Cannon82,
author = {H. I. Cannon},
title = {Flavors: A non-hierarchical approach to
object-oriented programming},
publisher = {Symbolics, Inc.},
address = {Cambridge, Mass.},
year = {1982},
OPTkey = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTedition = {},
OPTmonth = {},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@Article{ Cardelli83,
author = "Cardelli, Luca",
title = "The Functional Abstract Machine",
journal = "Polymorphism Newsletter",
year = "1983",
volume = "1",
number = "1",
month = jan,
}
@InCollection{ Cardelli84,
author = "Cardelli, Luca",
title = "A Semantics of Multiple Inheritance",
booktitle = "Semantics of Data Types, International Symposium",
publisher = Springer,
year = "1984",
series = lncs,
volume = "173",
pages = "51--68",
address = "Berlin, Heidelberg, New York",
}
@Article{ Cardelli85,
author = "Cardelli, Luca",
title = "Basic Polymorphic Typechecking",
journal = "Polymorphism Newsletter",
year = "1985",
volume = "2",
number = "1",
month = jan,
note = "Also appeared as Computing Science Technical Report 119, AT\&T Bell Laboratories, Murray Hill, NJ"
}
@InCollection{ Cardelli86,
author = "Cardelli, Luca",
title = "Amber",
booktitle = "Combinators and Functional Programming Languages",
publisher = Springer,
year = "1986",
editor = "G. Cousineau and Pierre-Louis Curien and B. Robinet",
pages = "21--47",
series = lncs,
volume = "242",
address = "Berlin, Heidelberg, New York",
}
@Article{ Cardelli88,
author = "Cardelli, Luca",
title = "A Semantics of Multiple Inheritance",
journal = "Information and Computation",
year = "1988",
volume = "76",
pages = "138--164",
}
@Article{ Cardelli95,
author = "Luca Cardelli",
title = "A Language with Distributed Scope",
journal = "Computing Systems",
volume = "8",
number = "1",
pages = "27--59",
year = "1995",
ISSN = "0895-6340",
URL = "file://www.research.digital.com/SRC/Obliq/Obliq.html",
note = "Short version in {\em Proceedings 22nd Annual ACM
Symposium on Principles of Programming Languages},
January, 1995",
}
@inproceedings{ CardelliGordon98:fossacs,
author = "Luca Cardelli and Andrew D. Gordon",
title = "Mobile Ambients",
booktitle = "Foundations of Software Science and Computation Structures: First International Conference, {FOSSACS '98}",
publisher = "Springer-Verlag, Berlin Germany",
year = "1998",
url = "citeseer.nj.nec.com/cardelli98mobile.html" }
@techreport{ CardelliMathesAbadi94:extensiblesyntax,
author = "Luca Cardelli and Florian Matthes and Martin Abadi",
title = "Extensible Syntax with Lexical Scoping",
institution = "DEC SRC",
number = "121",
pages = "41",
year = "1994",
url = "citeseer.csail.mit.edu/cardelli94extensible.html"
}
@Article{ CardelliWegner85,
author = "Cardelli, Luca and Wegner, Peter",
title = "On Understanding Types, Data Abstraction, and Polymorphism",
journal = "Computing Surveys",
year = "1985",
volume = "17",
pages = "471--522",
}
@Article{ Carter77,
author = "Carter, J. L.",
title = "A Case Study of a New Code Generation Technique for Compilers",
journal = "Commumications of the ACM",
year = "1977",
volume = "20",
pages = "914--920",
}
@Book{ ChangLee73,
author = "Chang, C. C. and Lee, R. C. T.",
title = "Symbolic Logic and Mechanical Theorem-Proving",
publisher = "Academic Press",
year = "1973",
address = "New York",
}
@InProceedings{ ChiricaMartin76,
author = "Chirica, L. M. and Martin, D. F.",
title = "An Algebraic Formulation of Knuthian Semantics",
booktitle = "Proceedings 17th IEEE Symposium on Foundations of Computing",
year = "1976",
pages = "127--136",
note = "appeared later in {\it Mathematical Systems Theory}"
}
@Article{ Church40,
author = "Church, Alonzo",
title = "A formulation of the simple theory of types",
journal = "Journal of Symbolic Logic",
year = "1940",
volume = "5",
pages = "56--68",
}
@Book{ Church41,
author = "Church, Alonzo",
title = "The Calculi of Lambda Conversion",
publisher = "Princeton University Press",
year = "1941",
note = "Reprinted 1963 by University Microfilms, Ann Arbor, MI",
address = "Princeton, NJ"
}
@Book{ Church56,
author = "Church, Alonzo",
title = "Introduction to Mathematical Logic, Volume I",
publisher = "Princeton University Press",
year = "1956",
address = "Princeton, NJ",
}
@inproceedings{ ClaessenLjunglof01,
author = {Koen Claessen and Peter Ljunglof},
title = {Typed Logical Variables in Haskell},
booktitle = {Electronic Notes in Theoretical Computer Science},
volume = {41},
issue = {1},
publisher = {Elsevier Science Publishers},
editor = {Graham Hutton},
year = {2001}
}
@Book{ ClarkTarnlund82,
author = "Clark, K. L. and T{\"a}rnlund, S.-A",
title = "Logic Programming",
publisher = "Academic Press",
year = "1982",
address = "New York",
}
@InProceedings{ ClarkeEtAl80,
author = "Clarke, T. and Gladstone, P. and Maclean, C. and Norman, A.",
title = "SKIM --- The S, K, I Reduction Machine",
booktitle = "Conference Record of the 1980 LISP Conference",
year = "1980",
pages = "128--135",
}
@inproceedings{ ClassicJava,
author = {Matthew Flatt and Shriram Krishnamurthi and Matthias Felleisen},
title = {A Programmer's Reduction Semantics for Classes and Mixins},
booktitle = {Formal Syntax and Semantics of Java},
year = {1999},
isbn = {3-540-66158-1},
pages = {241--269},
publisher = {Springer-Verlag},
address = {London, UK},
}
@InProceedings{ ClementEtAl86,
author = "Cl\'ement, D. and Despeyroux, J. and Despeyroux, T. and Kahn, Gilles",
title = "A Simple Applicative Language: Mini-ML",
booktitle = "{\lfp{1986}}",
year = "1986",
pages = "13--27",
}
@PhdThesis{ Clinger81,
author = {William D. Clinger},
title = {Foundations of Actor Semantics},
school = {MIT},
year = 1981,
month = may
}
@InProceedings{ Clinger82,
author = "Clinger, William",
title = "Nondeterministic Call by Need is Neither Lazy nor by Name",
booktitle = "{\lfp{1982}}",
year = "1982",
pages = "226--234",
}
@InProceedings{ Clinger84,
author = "Clinger, William",
title = "The {S}cheme 311 Compiler: An Exercise in Denotational Semantics",
booktitle = "{\lfp{1984}}",
year = "1984",
pages = "356--364",
month = aug,
}
@InProceedings{ Clinger:pldi98,
author = "William D.~Clinger",
title = "Proper Tail Recursion and Space Efficiency",
booktitle = "Proceedings of the ACM SIGPLAN '98 Conference on
Programming Language Design and Implementation",
OPTmonth = "June",
year = "1998",
pages = "174--185"
}
@InProceedings{ Clinger:pldi98,
author = "William D.~Clinger",
title = "Proper Tail Recursion and Space Efficiency",
booktitle = "Proceedings of the ACM SIGPLAN '98 Conference on
Programming Language Design and Implementation",
month = "June",
year = "1998",
pages = "174--185"
}
@InCollection{ ClingerFriedmanWand82,
author = "Clinger, William and Friedman, Daniel P. and Wand, Mitchell",
title = "A Scheme for a Higher-Level Semantic Algebra",
booktitle = "Algebraic Methods in Semantics",
publisher = "Oxford University Press",
year = "1985",
editor = "Maurice Nivat and John C. Reynolds",
pages = "237--250",
address = "Cambridge",
note = "Proceedings of US-French
Seminar on the Application of Algebra to Language Definition and Compilation,
Fontainebleau, France, 1982"
}
@InProceedings{ ClingerHansen94,
author = {William D. Clinger and Lars Thomas Hansen},
title = {Lambda, the Ultimate Label, or a Simple Optimizing
Compiler for {S}cheme},
booktitle = lfp94,
year = 1994,
pages = {128-139}
}
@InProceedings{ ClingerHansen97,
author = "William D.~Clinger and Lars T.~Hansen",
title = "Generational Garbage Collection and the Radioactive Decay Model",
booktitle = "Proceedings of the ACM SIGPLAN '97 Conference on
Programming Language Design and Implementation",
month = "June",
year = "1997",
pages = "97--108"
}
@inproceedings{ ClingerRees:MacrosThatWork91,
author = {William Clinger and Jonathan Rees},
title = {Macros that work},
booktitle = popl,
year = {1991},
isbn = {0-89791-419-8},
pages = {155--162},
location = {Orlando, Florida, United States},
doi = {http://doi.acm.org/10.1145/99583.99607},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@Unpublished{ ClingerWand96,
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},
}
@Article{ Clingeretal:hosc99,
author = "William D.~Clinger and Anne H.~Hartheimer and Eric Ost",
title = "Implementation Strategies for First-class Continuations",
journal = "Journal of Higher Order and Symbolic Computation",
year = "1999",
volume = "12",
pages = "7--45"
}
@Article{ Clingeretal:hosc99,
author = "William D.~Clinger and Anne H.~Hartheimer and Eric Ost",
title = "Implementation Strategies for First-class Continuations",
journal = "Journal of Higher Order and Symbolic Computation",
year = "1999",
volume = "12",
pages = "7--45"
}
@Book{ Cohn65,
author = "Cohn, P. M.",
title = "Universal Algebra",
publisher = "Harper \&\ Row",
year = "1965",
address = "New York",
}
@InCollection{ Cointe88,
author = "Cointe, P.",
title = "The ObjVlisp Kernel: A Reflective Lisp Architecture
to define a Uniform Object-Oriented System",
booktitle = "Meta-Level Architectures and Reflection",
publisher = "North-Holland",
year = "1988",
editor = "Maes, P. and Nardi, D.",
address = "Amsterdam",
}
@InProceedings{ ColbyEtAl-coots98,
author = "Christopher Colby and Lalita Jategaonkar Jagadeesan
and Radha Jagadeesan and Konstantin L{\"a}ufer and
Carlos Puchol",
booktitle = "Proceedings of the 1998 USENIX Conference on Object
Oriented Technologies and Systems.",
title = "Objects and Processes in {Triveni}: {A} case study from
telecommunications in Java",
year = "1998",
url = "www.cs.luc.edu/~radha/pubs.html",
month = apr,
organization = "USENIX",
}
@inproceedings{ ColbyEtAl-entcs2000,
author = "Christopher Colby and Lalita Jategaonkar Jagadeesan
and Radha Jagadeesan and Konstantin L{\"a}ufer and
Carlos Puchol",
title = "The Semantics of {Triveni}: A Process-Algebraic {API} for
Threads + Events",
booktitle = "Electronic Notes in Theoretical Computer Science",
volume = "14",
publisher = "Elsevier Science Publishers",
editor = "Rance Cleaveland and Michael Mislove and Philip Mulry",
year = "2000"
}
@InProceedings{ ColbyEtAl-iccl98,
author = "Christopher Colby and Lalita Jategaonkar Jagadeesan
and Radha Jagadeesan and Konstantin L{\"a}ufer and
Carlos Puchol",
title = "Design and Implementation of {T}riveni: a
Process-algebraic {API} for Threads + Events",
booktitle = "Proceedings of the 1998 International Conference on
Computer Languages",
publisher = "IEEE Computer Society Press",
year = "1998",
ISBN = "0-780-35005-7, 0-8186-8454-2, 0-8186-8456-9",
pages = "58--67",
abstract = "We describe \emph{Triveni}, a framework and API for
integrating threads and events. The \emph{design} of
Triveni is based on an algebra, including preemption
combinators, of processes. Triveni is compatible with
existing threads standards, such as Pthreads and Java
threads, and with the event models structured on the
Observer pattern. We describe the software architecture
and algorithms underlying a concrete
\emph{implementation} of Triveni in Java. This
environment includes specification-based testing of
safety properties. The results described in this paper
have been used to integrate process-algebraic methods
into (concurrent) object oriented programming [8].",
}
@InProceedings{ Consel90,
author = "Charles Consel",
title = "Binding Time Analysis for Higher Order Untyped
Functional Languages",
booktitle = "{\lfp{1990}}",
year = "1990",
pages = "264--272",
}
@TechReport{ ConselKhoo92,
author = "Charles Consel and Siau Cheng Khoo",
title = "On-line \&\ Off-line Partial Evaluation: Semantic
Specifications and Correctness Proofs",
institution = "Yale University Department of Computer Science",
year = "1992",
number = "YALEU/DCS/RR-912",
month = jun,
}
@Article{ ConstableZlatin84,
author = "Constable, R. L. and Zlatin, D. R.",
title = "The Type Theory of PL/CV3",
journal = "ACM Transactions on Programming Languages and Systems",
year = "1984",
volume = "6",
pages = "94--117",
}
@Article{ Cook78,
author = "Cook, Steven A.",
title = "Soundness and Completeness of an Axiom System for
Program Verification",
journal = "SIAM Journal on Computing",
year = "1978",
volume = "7",
pages = "70--90",
}
@Unpublished{ Cook87,
author = "Cook, W.",
title = "A self-ish model of inheritance",
note = "manuscript",
year = "1987",
}
@Article{ Coppo84,
author = "Coppo, M.",
title = "Completeness of Type Assignment in Continuous Lambda Models",
journal = "Theoretical Computer Science",
year = "1984",
volume = "29",
pages = "309--324",
}
@Article{ Correll78,
author = "Correll, C. H.",
title = "Proving Programs Correct through Refinement",
journal = "Acta Informatica",
year = "1978",
volume = "9",
pages = "121--132",
}
@Article{ Courcelle83,
author = "Courcelle, Bruno",
title = "Fundamental Properties of Infinite Trees",
journal = "Theoretical Computer Science",
year = "1983",
volume = "25",
OPTnumber = "",
pages = "95--169",
OPTmonth = "",
OPTnote = ""
}
@InProceedings{ CousotCousot77,
author = "Patrick Cousot and Radhia Cousot",
title = "Abstract interpretation: a unified lattice model for
static analysis of programs by construction or
approximation of fixpoints",
booktitle = popl4,
year = "1977",
OPTeditor = "",
pages = "238-252",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
OPTnote = ""
}
@InProceedings{ Cregut90,
author = "P. Cr{\'e}gut",
title = "An abstract machine for the normalization of
$\lambda$-terms",
booktitle = lfp90,
organization = "ACM",
month = jun,
year = "1990",
pages = "333--340",
checked = "19940806",
source = "Dept. Library",
abstract = "Two abstract machines reducing terms to their full
normal form are presented in this paper. They are based
on Krivine's abstract machine which uses an environment
to store arguments of function calls. A proof of their
correctness is then stated in the abstract framework of
$\lambda\sigma$-calculus.",
}
@InProceedings{ CroleGordon94,
author = "R. L. Crole and A. D. Gordon",
title = "A Sound Metalogical Semantics for Input/Output
Effects",
booktitle = {Computer science logic: 8th workshop, CSL '94},
editor = {Leszek Pacholski and Jerzy Tiuryn},
publisher = springer,
series = lncs,
volume = 933,
address = springeraddr,
year = 1995,
pages = "339--353",
}
@Book{ CurryFeys58,
author = "Curry, Haskell B. and Feys, R.",
title = "Combinatory Logic",
publisher = "North-Holland",
year = "1958",
volume = "1",
address = "Amsterdam",
}
@Book{ CurryHindleySeldin72,
author = {Curry, Haskell B. and Feys, R. and Seldin, J. P.},
title = {Combinatory Logic},
publisher = {North-Holland},
year = 1972,
volume = 2
}
@proceedings{ DBLP:conf/ac/2000appsem,
editor = {Gilles Barthe and
Peter Dybjer and
Luis Pinto and
Jo{\~a}o Saraiva},
title = {Applied Semantics, International Summer School, APPSEM 2000,
Caminha, Portugal, September 9-15, 2000, Advanced Lectures},
booktitle = {APPSEM},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2395},
year = {2002},
isbn = {3-540-44044-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{ DGR02,
author = "Olivier Danvy and Bernd Grobauer and Morten Rhiger",
title = "A Unifying Approach to Goal-Directed Evaluation",
journal = "New Generation Computing",
volume = "20",
pages = "53-73",
year = "2002",
}
@Book{ DahlDijkstraHoare72,
author = "Dahl, O. J. and Dijkstra, E. W. and Hoare, C. A. R.",
title = "Structured Programming",
publisher = "Academic Press",
year = "1972",
address = "London",
}
@InCollection{ DahlHoare72,
author = "Dahl, O. J. and Hoare, C. A. R.",
title = "Hierarchical Program Structures",
booktitle = "Structured Programming",
publisher = "Academic Press",
year = "1972",
editor = "Dahl, O. J. and Dijkstra, E. W. and Hoare, C. A. R.",
pages = "175--220",
address = "London",
}
@InProceedings{ DamasMilner82,
author = "Damas, L. and Milner, R.",
title = "Principal Type-Schemes for Functional Programs",
booktitle = "{\popl{9th}}",
year = "1982",
pages = "207--212",
}
@InProceedings{ DamianDanvy-icfp00,
author = {Daniel Damian and Olivier Danvy},
title = {Syntactic Accidents in Program Analysis},
booktitle = icfp,
year = 2000,
month = sep,
}
@inproceedings{ DanvyFilinski-lfp90,
author = "O. Danvy and A. Filinski",
title = "Abstracting Control",
booktitle = "Proceedings of the 1990 {ACM} Conference on {LISP} and Functional Programming, Nice",
publisher = "ACM",
address = "New York, NY",
pages = "151--160",
year = "1990",
url = "citeseer.ist.psu.edu/danvy90abstracting.html" }
@Article{ DanvyFilinski92,
author = "Olivier Danvy and Andrzej Filinski",
title = "Representing Control: {A} study of the {CPS}
transformation",
year = "1992",
url = "http://www.cs.cmu.edu/afs/cs.cmu.edu/user/andrzej/pub/RC.ps.Z",
month = dec,
number = "4",
pages = "361--391",
volume = "2",
journal = "Mathematical Structures in Computer Science",
}
@InProceedings{ DanvyMalmkjaer88,
author = {Olivier Danvy and Karoline Malmkj{\ae}r},
title = {Intensions and Extensions in a Reflective Tower},
booktitle = lfp88,
year = 1988,
pages = {327-341}
}
@Article{ DanvyNielsen:TCS03,
author = "Olivier Danvy and Lasse R. Nielsen",
title = "A First-Order One-Pass {CPS} Transformation",
journal = "Theoretical Computer Science",
year = 2003,
volume = 308,
number = "1-3",
pages = "239-257",
OPTmonth = Nov
}
@TechReport{ DarringerLaventhal78,
author = "Darringer, J. A. and Laventhal, M. S.",
title = "A Study of the Use of Abstractions in Program Specification and Verification",
institution = "IBM",
year = "1978",
type = "Research Report",
number = "RC 7184",
}
@Book{ Davis65,
author = "Davis, Martin",
title = "The Undecidable",
publisher = "Raven Press",
year = "1965",
address = "Hewlett, NY",
}
@InProceedings{ DeMilloLipton79,
author = "DeMillo, R. A. and Lipton, R. J.",
title = "Some Connections between Mathematical Logic and Complexity Theory",
booktitle = "Proceedings 11th Annual ACM Symposium on Theory of Computing",
year = "1979",
pages = "153--159",
}
@InProceedings{ DemersDonahue80,
author = "Demers, Alan J. and Donahue, James E.",
title = "Data Types, Parameters and Type Checking",
booktitle = "{\popl{7th}}",
year = "1980",
pages = "12--23",
}
@Book{ DenningDennisQualitz78,
author = "Denning, P. J. and Dennis, J. B. and Qualitz, J. E.",
title = "Machines, Languages and Computation",
publisher = "Prentice-Hall",
year = "1978",
address = "Englewood Cliffs, NJ",
}
@TechReport{ Deransart78,
author = "Deransart, P.",
title = "Technique de Preuve par Attributs Appliqu\'ee \`a un Compilateur {Lisp}",
institution = "IRIA",
year = "1978",
type = "Research Report",
number = "271",
month = jan,
}
@Article{ Dijkstra68,
author = "Dijkstra, Edsger W.",
title = "Go To Statement Considered Harmful",
journal = "Communications of the ACM",
year = "1968",
volume = "11",
pages = "147--148",
}
@Article{ Dijkstra71,
author = "Dijkstra, Edsger W.",
title = "Hierarchical Ordering of Sequential Processes",
journal = "Acta Informatica",
year = "1971",
volume = "1",
pages = "115--138",
}
@InCollection{ Dijkstra72,
author = "Dijkstra, Edsger W.",
title = "Notes on Structured Programming",
booktitle = "Structured Programming",
publisher = "Academic Press",
year = "1972",
editor = "Dahl, O. J. and Dijkstra, Edsger W. and Hoare, C. A. R.",
address = "London",
}
@Article{ Dijkstra75,
author = "Dijkstra, Edsger W.",
title = "Guarded Commands, Nondeterminancy and Formal Derivation of Pro\-grams",
journal = "Communications of the ACM",
year = "1975",
volume = "18",
pages = "453--457",
}
@Book{ Dijkstra76a,
author = "Dijkstra, Edsger W.",
title = "A Discipline of Programming",
publisher = "Prentice-Hall",
year = "1976",
address = "Englewood Cliffs, N. J.",
}
@InCollection{ Dijkstra76b,
author = "Dijkstra, Edsger W.",
title = "The Effective Arrangement of Logical Systems",
booktitle = "Mathematical Founda\-tions of Computer Science 1976",
publisher = Springer,
year = "1976",
editor = "A. Mazurkiewicz",
series = lncs,
pages = "39--51",
volume = "45",
address = "Berlin, Heidelberg, New York",
}
@Article{ Donahue79,
author = "Donahue, James",
title = "On the Semantics of `Data Type'",
journal = "SIAM Journal on Computing",
year = "1979",
volume = "8",
pages = "546--560",
}
@Book{ Dybvig2e,
author = "R. Kent Dybvig",
title = "The {Scheme} programming language: {ANSI Scheme}",
publisher = "Pren{\-}tice-Hall PTR",
address = "Upper Saddle River, NJ 07458, USA",
edition = "Second",
pages = "xii + 248",
year = "1996",
bibdate = "Mon Feb 24 15:49:20 MST 1997",
acknowledgement = ack-nhfb,
}
@Book{ Dybvig87,
author = "Dybvig, Kent",
title = "The Scheme Programming Language",
publisher = "Prentice-Hall",
year = "1987",
address = "Englewood Cliffs, NJ",
}
@article{ DybvigHiebBruggeman:LASC92,
address = {Hingham, MA, USA},
author = {Dybvig, R. K. and Hieb, Robert and Bruggeman, Carl },
citeulike-article-id = {162160},
issn = {0892-4635},
journal = {Lisp Symb. Comput.},
keywords = {macros scheme syntax-case},
month = {December},
number = {4},
pages = {295--326},
priority = {0},
publisher = {Kluwer Academic Publishers},
title = {Syntactic abstraction in Scheme},
url = {http://portal.acm.org/citation.cfm?id=173620},
volume = {5},
year = {1992},
source = {citulike:samth}
}
@article{ Earley:cacm70,
author = {Jay Earley},
title = {An efficient context-free parsing algorithm},
journal = {Commun. ACM},
volume = {13},
number = {2},
year = {1970},
issn = {0001-0782},
pages = {94--102},
doi = {http://doi.acm.org/10.1145/362007.362035},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@TechReport{ Ehrich78,
author = "Ehrich, H. D.",
title = "Extensions and Implementations of Abstract Data
Type Specifications",
institution = "Abteilung Informatik, Universitat Dartmund",
year = "1978",
type = "Bericht",
number = "55/78",
}
@Article{ EhrigEtAl82,
author = "Ehrig, H. and Kreowski, H.-J. and Mahr, B. and
Padawitz, P.",
title = "Algebraic Implementation of Abstract Data Types",
journal = "Theoretical Computer Science",
year = "1982",
volume = "20",
pages = "209--263",
}
@InProceedings{ EhrigKreowskiPadowitz78,
author = "Ehrig, H. and Kreowski, H.-J. and Padowitz, P.",
title = "Stepwise Specification and Implementation of Abstract Data Types",
booktitle = "Proceedings 5th International Colloquium on Automata, Languages, and Programming",
year = "1978",
}
@InProceedings{ EhrigKreowskiPadowitz80,
author = "Ehrig, H. and Kreowski, H.-J. and Padowitz, P.",
title = "Algebraic Implementation of Abstract Data Types:
Concept, Syntax, Semantics and Correctness",
booktitle = "Automata, Languages and Programming, Seventh
Colloquium",
year = "1980",
}
@InProceedings{ Elgot75,
author = "Elgot, Calvin C.",
title = "Monadic Computation and Iterative Algebraic Theories",
booktitle = "Logic Colloquium '73",
year = "1975",
editor = "H. E. Rose and J. C. Shepherdson",
publisher = "North-Holland",
address = "Amsterdam",
note = "Proceedings of the Logic Colloquium, Bristol, 1973",
pages = "175--230",
}
@Article{ ElgotSnyder77,
author = "Elgot, Calvin C. and Snyder, Larry",
title = "On the Many Facets of
Lists",
journal = "Theoretical Computer Science",
year = "1977",
volume = "5",
pages = "275--306",
}
@Book{ EllisStroustrup90,
author = "Ellis, M. A. and Stroustrup, B.",
title = "The Annotated C++ Reference Manual",
publisher = "Addison-Wesley",
year = "1990",
address = "Reading, MA",
}
@Book{ Enderton72,
author = "Enderton, H. B",
title = "A Mathematical Introduction to Logic",
publisher = "Academic Press",
year = "1972",
address = "New York and London",
}
@InCollection{ Ershov78,
author = "Ershov, A. P.",
title = "On the Essence of Compilation",
booktitle = "Formal Descriptions of Programming Concepts",
publisher = "North-Holland",
year = "1978",
editor = "E. J. Neuhold",
pages = "391--420",
address = "Amsterdam",
}
@Article{ Facile,
author = "Alessandro Giacalone and Prateek Mishra and Sanjiva Prasad",
title = "Facile: A Symmetric Integration of Concurrent and
Functional Programming",
journal = "International Journal of Parallel Programming",
year = 1989,
volume = "18",
number = "2",
pages = "121--160",
OPTmonth = "",
OPTnote = ""
}
@MastersThesis{ Federhen80,
author = "Federhen, Scott",
title = "A Mathematical Semantics for {PLANNER}",
school = "University of Maryland",
year = "1980",
}
@inproceedings{ Felleisen-popl88,
author = {Matthias Felleisen},
title = {The theory and practice of first-class prompts},
booktitle = popl,
year = {1988},
isbn = {0-89791-252-7},
pages = {180--190},
location = {San Diego, California, United States},
doi = {http://doi.acm.org/10.1145/73560.73576},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@PhdThesis{ Felleisen87,
author = "Matthias Felleisen",
year = 1987,
title = "The Calculi of Lambda-v-cs Conversion: {A} Syntactic Theory of Control and State
in Imperative Higher-Order Programming Languages",
school = "Indiana University",
}
@inproceedings{ Felleisen:oxford03,
author="M. Felleisen",
title="Developing Interactive Web Programs",
year=2003,
booktitle="{A}dvanced {F}unctional {P}rogramming",
editor="Johan Jeuring and Simon Peyton Jones",
publisher= springer,
address = springeraddr,
series=lncs,
number=2638,
pages="100-128"
}
@Misc{ FelleisenFlatt02,
OPTkey = {},
author = {Matthias Felleisen and Matthew Flatt},
title = {Programming Languages and Lambda Calculi},
howpublished = {notes for Utah CS6520},
year = {2002},
month = jan,
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@Article{ Felleisenetal87,
author = "M. Felleisen and D. P. Friedman and E. Kohlbecker and
B. Duba",
title = "A syntactic theory of sequential control",
journal = "Theoretical Computer Science",
volume = "52",
number = "3",
pages = "205--237",
year = "1987",
coden = "TCSCDI",
ISSN = "0304-3975",
bibdate = "Sat Nov 22 13:29:49 MST 1997",
acknowledgement = ack-nhfb,
classification = "C4210 (Formal logic); C4220 (Automata theory); C4240
(Programming and algorithm theory)",
corpsource = "Dept. of Comput. Sci., Indiana Univ., Bloomington, IN,
USA",
keywords = "abstract machine; algebraic extension; calculus;
call/cc; context-free languages; diamond property;
evaluation function; formal logic; lambda /sub nu /
calculus; lambda calculus; machine semantics;
nonfunctional control operators; programming language;
programming theory; rewriting machine; sequential
control; sequential machines; standardization theorem;
syntactic theory",
pubcountry = "Netherlands A03",
treatment = "T Theoretical or Mathematical",
}
@InProceedings{ Felleisenetal88,
author = "Matthias Felleisen and Mitchell Wand and Daniel P.
Friedman and Bruce Duba",
title = "Abstract Continuations: {A} Mathematical Semantics for
Handling Functional Jumps",
booktitle = "Proceedings of the 1988 ACM Symposium on LISP and
Functional Programming",
address = "Salt Lake City, Utah",
month = jul,
year = "1988",
}
@TechReport{ Fessenden83,
author = "Fessenden, Carol and Clinger, William and Friedman,
Daniel P. and Haynes, Christopher T.",
title = "Scheme 311 Version 4 Reference Manual",
institution = "Indiana University Computer
Science Department",
year = "1983",
type = "Technical Report",
number = "137",
month = feb,
}
@inproceedings{ Filinski:popl99,
author = "Andrzej Filinski",
title = "Representing Layered Monads",
booktitle = "{\popl{26th}}",
pages = "175--188",
year = "1999",
url = "citeseer.nj.nec.com/filinski99representing.html" }
@InProceedings{ Filman-Havelund02,
key = "Filman \& Havelund",
author = "Robert E. Filman and Klaus Havelund",
title = "Source-Code Instrumentation and Quantification of
Events",
pages = "45--49",
booktitle = "FOAL 2002 Proceedings: Foundations of Aspect-Oriented
Languages Workshop at AOSD 2002",
year = "2002",
editor = "Gary T. Leavens and Ron Cytron",
organization = "Department of Computer Science, Iowa State
University",
series = "Technical Report 02-06",
OPTnumber = "02-06",
month = apr,
url = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-06/TR.pdf",
}
@Book{ FilmanFriedman84,
author = "Filman, Robert E. and Friedman, Daniel P.",
title = "Coordinated Computing: Tools and Techniques for Distributed Software",
publisher = "McGraw-Hill",
year = "1984",
address = "New York",
}
@InProceedings{ Fischer72,
author = "Fischer, Michael J.",
title = "Lambda-Calculus Schemata",
booktitle = "Proceedings ACM Conference on Proving Assertions about Programs",
year = "1972",
address = "Los Cruces",
note = "SIGPLAN Notices, 7(1), January 1972",
pages = "104--109",
}
@Book{ FischerLeBlanc88,
author = "Fischer, Charles N. and LeBlanc, Richard J.",
title = "Crafting a Compiler",
publisher = "Benjamin/Cummings",
year = "1988",
address = "Menlo Park, CA",
}
@TechReport{ FlanaganFelleisen95,
author = {Cormac Flanagan and Matthias Felleisen},
title = {Set-based analysis for full scheme and its use in
soft-typing},
institution = {Department of Computer Science, Rice University},
year = {1995},
OPTkey = {},
OPTtype = {},
number = {COMP TR95-253},
OPTaddress = {},
month = oct,
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@InProceedings{ FlanaganFelleisen95:popl,
author = "Cormac Flanagan and Matthias Felleisen",
title = "The semantics of future and its use in program
optimization",
booktitle = popl22,
year = "1995",
ISBN = "0-89791-692-1",
pages = "209--220",
bibdate = "Mon May 3 12:52:30 MDT 1999",
url = "http://www.acm.org:80/pubs/citations/proceedings/plan/199448/p209-flanagan/",
abstract = "The {\bf future} annotations of MultiLisp provide a
simple method for taming the implicit parallelism of
functional programs. Past research concerning {\bf
future}s has focused on implementation issues. In this
paper, we present a series of operational semantics for
an idealized functional language with {\bf future}s
with varying degrees of intensionality. We develop a
set-based analysis algorithm from the most intensional
semantics, and use that algorithm to perform {\em
touch\/} optimization on programs. Experiments with the
Gambit compiler indicates that this optimization
substantially reduces program execution times.",
acknowledgement = ack-nhfb,
keywords = "algorithms; experimentation; languages; theory",
subject = "{\bf D.3.4} Software, PROGRAMMING LANGUAGES,
Processors, Optimization. {\bf D.3.2} Software,
PROGRAMMING LANGUAGES, Language Classifications,
MULTILISP. {\bf D.3.1} Software, PROGRAMMING LANGUAGES,
Formal Definitions and Theory, Semantics. {\bf F.3.2}
Theory of Computation, LOGICS AND MEANINGS OF PROGRAMS,
Semantics of Programming Languages, Operational
semantics.",
}
@InProceedings{ FlanaganFelleisen97,
author = {Cormac Flanagan and Matthias Felleisen},
title = {Componential Set-Based Analysis},
booktitle = pldi97,
year = 1997,
organization = {ACM},
month = jun,
pages = {235-248}
}
@Article{ FlanaganFelleisen99,
author = "Cormac Flanagan and Matthias Felleisen",
title = "Componential set-based analysis",
journal = "ACM Transactions on Programming Languages and
Systems",
volume = "21",
number = "2",
pages = "370--416",
month = mar,
year = "1999",
coden = "ATPSDT",
ISSN = "0164-0925",
bibdate = "Fri Oct 1 19:16:48 MDT 1999",
url = "http://www.acm.org:80/pubs/citations/journals/toplas/1999-21-2/p370-flanagan/",
abstract = "Set-based analysis (SBA) produces good predictions
about the behavior of functional and object-oriented
programs. The analysis proceeds by inferring {\em
constraints\/} that characterize the data flow
relationships of the analyzed program. Experiences with
MrSpidey, a static debugger based on SBA, indicate that
SBA can adequately deal with programs of up to a couple
of thousand lines of code. SBA fails, however, to cope
with larger programs because it generates systems of
constraints that are at least linear, and possibility
quadratic, in the size of the analyzed program. This
article presents theoretical and practical results
concerning methods for reducing the size of constraint
systems. The theoretical results include of
proof-theoretic characterization of the {\em observable
behavior\/} of constraint systems for program
components, and a complete algorithm for deciding the
observable equivalence of constraint systems. In the
course of this development we establish a close
connection between the observable equivalence of
constraint systems and the equivalence of regular-tree
grammars. We then exploit this connection to adapt a
variety of algorithms for simplifying grammars to the
problem of simplifying constraint systems. Based on the
resulting algorithms, we have developed {\em
componential set-based analysis\/}, a modular and
polymorphic variant of SBA. Experimental results verify
the effectiveness of the simplification algorithms and
the componential analysis. The simplified constraint
systems are typically an order of magnitude smaller
than the original systems. These reductions in size
produce significant gains in the speed of the
analysis.",
acknowledgement = ack-nhfb,
keywords = "algorithms; languages; performance; theory",
subject = "{\bf D.2.5} Software, SOFTWARE ENGINEERING, Testing
and Debugging, Debugging aids. {\bf D.2.6} Software,
SOFTWARE ENGINEERING, Programming Environments. {\bf
D.3.4} Software, PROGRAMMING LANGUAGES, Processors,
Debuggers. {\bf D.3.4} Software, PROGRAMMING LANGUAGES,
Processors, Optimization. {\bf F.3.1} Theory of
Computation, LOGICS AND MEANINGS OF PROGRAMS,
Specifying and Verifying and Reasoning about Programs,
Mechanical verification. {\bf F.3.3} Theory of
Computation, LOGICS AND MEANINGS OF PROGRAMS, Studies
of Program Constructs, Type structure. {\bf D.2.5}
Software, SOFTWARE ENGINEERING, Testing and Debugging,
Symbolic execution.",
}
@Article{ Flatt-Krishnamurthi-Felleisen99:Classic-Java,
author = "M. Flatt and S. Krishnamurthi and M. Felleisen",
title = "A Programmer's Reduction Semantics for Classes and
Mixins",
journal = "Lecture Notes in Computer Science",
volume = "1523",
pages = "241--269",
year = "1999",
coden = "LNCSD9",
ISSN = "0302-9743",
bibdate = "Mon Sep 13 16:57:02 MDT 1999",
acknowledgement = ack-nhfb,
}
@InProceedings{ Flatt01:Jiazzi,
author = "Sean McDirmid and Matthew Flatt and Wilson Hsieh",
title = "Jiazzi: New Age Components for Old Fashioned Java",
booktitle = oopsla,
pages = "211--222",
month = oct,
year = "2001",
keywords = "olit oopsla01",
url = "http://www.cs.utah.edu/plt/jiazzi/publications.html",
}
@inproceedings{ Flatt:icfp02,
author = {Matthew Flatt},
title = {Composable and compilable macros: you want it when?},
booktitle = icfp,
year = {2002},
pages = {72-83},
ee = {http://doi.acm.org/10.1145/581478.581486},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InProceedings{ FlattFelleisen98,
author = "Matthew Flatt and Matthias Felleisen",
title = "Units: Cool Modules for {HOT} Languages",
booktitle = "{ACM SIGPLAN Conference on Programming Language Design
and Implementation (PLDI)} , {M}ontreal, {C}anada",
year = "1998",
pages = "236--248",
fullurl = "http://www.acm.org/pubs/articles/proceedings/pldi/277650/p236-flatt/p236-flatt.pdf",
genterms = "ALGORITHMS, DESIGN, LANGUAGES",
categories = "D.2.2 Software, SOFTWARE ENGINEERING, Design Tools and
Techniques, Modules and interfaces. D.3.2 Software,
PROGRAMMING LANGUAGES, Language Classifications,
SCHEME. D.3.2 Software, PROGRAMMING LANGUAGES, Language
Classifications, ML. F.3.3 Theory of Computation,
LOGICS AND MEANINGS OF PROGRAMS, Studies of Program
Constructs, Type structure.",
annote = "incomplete",
}
Lexer and parser generators in Scheme.
Matthew Flatt, Benjamin McMullan, Scott Owens and Olin Shivers.
In \emph{Proceedings of the Fifth Workshop on
Scheme and Functional Programming},
pages 41--52, Snowbird, Utah, September 2004.
@InProceedings{ FlattEtAl:SW04,
author = {Matthew Flatt and Benjamin McMullan and Scott Owens
and Olin Shivers},
title = {Lexer and parser generators in Scheme},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of the Fifth Workshop on
Scheme and Functional Programming},
pages = {41-52},
year = {2004},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
month = sep,
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {}
}
@InProceedings{ FlonMisra79,
author = "Flon, Lawrence and Misra, J.",
title = "A Unified Approach to the Specification and Verification of Abstract Data Types",
booktitle = "Proceedings: Specifications of Reliable Software",
year = "1979",
pages = "162--169",
series = "IEEE Catalog",
number = "79 CH1401-9C",
}
@InProceedings{ FlonSuzuki78,
author = "Flon, Lawrence and Suzuki, N.",
title = "Consistent and Complete
Proof Rules for the Total Correctness of Parallel Programs",
booktitle = "Proceedings 19th Symposium on Foundations of Computer Science",
year = "1978",
address = "Ann Arbor",
}
@InCollection{ Floyd67,
author = "Floyd, Robert W.",
title = "Assigning Meanings to Programs",
series = "Symposia in Applied Mathematics",
booktitle = "Mathematical Aspects of Computer Science",
volume = "19",
year = "1967",
editor = "J. T. Schwartz",
pages = "19--32",
publisher = "American Mathematical Society",
address = "Providence, RI",
}
M. Fowler and K. Scott. UML Distilled: Applying the Standard Object Modeling Language. Addison-Wesley, New York, 1997.
@InProceedings{ Fokkinga74,
author = "Fokkinga, M. M.",
title = "Inductive Assertion Patterns for Recursive Procedures",
booktitle = "Proceedings Colloquium on Programming",
year = "1974",
pages = "221--233",
address = "Paris",
}
@InCollection{ Fokkinga81,
author = "Fokkinga, M. M.",
title = "On the Notion of Strong Typing",
booktitle = "Algorithmic Languages",
publisher = "North-Holland",
year = "1981",
editor = "deBakker and van Vliet",
pages = "305--320",
address = "Amsterdam",
}
@Article{ FortuneLeivantO'Donnell83,
author = "Fortune, Steven and Leivant, Daniel and O'Donnell, Michael",
title = "The Expressiveness of Simple and Second-Order Type
Structures",
journal = "Journal of the ACM",
year = "1983",
volume = "30",
pages = "151--185",
}
@Book{ Fowler97:UMLDistilled,
author = {Martin Fowler and Kenall Scott},
title = {{UML} Distilled: Applying the Standard Object Modeling Language},
publisher = {Addison-Wesley},
year = {1997},
OPTkey = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
address = {New York},
OPTedition = {},
OPTmonth = {},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@TechReport{ FradetLeMetayer89,
author = "Fradet, Pierre and Le M\'etayer, Daniel",
title = "Compilation of Lambda-Calculus into Functional Machine Code",
institution = "IRISA",
year = "1989",
type = "Technical Report",
}
@InProceedings{ FrancezLehmannPnueli80,
author = "Francez, Nissim and Lehmann, Daniel J. and Pnueli, Amir",
title = "A Linear History Semantics for Distributed Languages",
booktitle = "21st Annual Symposium on Foundations of Computer Science",
year = "1980",
pages = "143--152",
address = "Syracuse",
}
@Book{ Friedman74,
author = "Friedman, Daniel P.",
title = "The Little LISPer",
publisher = "Science Research Associates",
year = "1974",
address = "Palo Alto, CA",
}
@Book{ FriedmanEtAl92,
author = "Friedman, Daniel P. and Wand, Mitchell and Haynes,
Christopher T.",
title = "Essentials of Programming Languages",
publisher = "MIT Press",
address = "Cambridge, MA",
year = "1992",
note = "Also McGraw-Hill, Chicago, 1992",
}
@Book{ FriedmanFelleisen87,
author = "Friedman, Daniel P. and Felleisen, Matthias",
title = "The Little LISPer",
publisher = "MIT Press",
year = "1987",
address = "Cambridge, MA",
edition = "Trade",
}
@InProceedings{ FriedmanHaynes84,
author = "Daniel P. Friedman and Christopher T. Haynes",
title = "Continuations and Coroutines: An Exercise in Metaprogramming",
booktitle = "{\lfp{1984}}",
year = "1984",
pages = "293--298",
month = aug,
}
@InProceedings{ FriedmanHaynes85,
author = "Friedman, Daniel P. and Haynes, Christopher T.",
title = "Constraining Control",
booktitle = "{\popl{12th}}",
year = "1985",
}
@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,
}
@InProceedings{ FriedmanWand84,
author = "Friedman, Daniel P. and Wand, Mitchell",
title = "Reification: Reflection without Metaphysics",
booktitle = "{\lfp{1984}}",
year = "1984",
pages = "348-355",
month = aug,
}
@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",
}
@Book{ FriedmanWand08,
author = "Daniel P. Friedman and Mitchell Wand",
title = "Essentials of Programming Languages",
publisher = "MIT Press",
year = {2008},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
address = "Cambridge, MA",
edition = {Third},
OPTmonth = {},
OPTnote = {},
OPTannote = {}
}
@InProceedings{ FriedmanWise76a,
author = "Friedman, Daniel P. and Wise, David S.",
title = "An Environment for Multiple-valued Recursive Procedures",
booktitle = "2nd Colloque sur la Programmation",
year = "1976",
publisher = "Dunod",
address = "Paris",
}
@InCollection{ FriedmanWise76b,
author = "Friedman, Daniel P. and Wise, David S.",
title = "{\it Cons} should not Evaluate its Arguments",
booktitle = "Automata, Languages and Programming",
publisher = "Edinburgh University Press",
year = "1976",
editor = "S. Michaelson and R. Milner",
pages = "257--284",
address = "Edinburgh",
}
Richard P. Gabriel, Jon L White, and Daniel G. Bobrow. CLOS:
Integrating ObjectOriented and Functional Programming. In
Communications of the ACM 34(9), pp. 28-38, September, 1991.
@TechReport{ FriedmanWise78,
author = "Friedman, Daniel P. and Wise, David S.",
title = "Applicative Multiprogramming",
institution = "Indiana University Computer Science Department",
year = "1978",
type = "Technical Report",
number = "72",
month = jan,
address = "Bloomington, IN",
}
@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",
}
@InProceedings{ FuhMishra88,
author = "Fuh, Y.-C. and Mishra, P.",
title = "Type Inference with Subtypes",
booktitle = "Proceedings European Symposium on Programming",
year = "1988",
pages = "94--114",
}
@Article{ GabrielWhiteBobrow91,
author = {Richard P. Gabriel and Jon L White and Daniel G. Bobrow},
title = {{CLOS}: Integrating Object-Oriented and Functional Programming},
journal = {Communications of the ACM},
year = {1991},
OPTkey = {},
volume = {34},
number = {9},
month = sep,
pages = {28-38},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@Article{ GallerFischer64,
author = "Galler, Bernard A. and Fischer, Michael J.",
title = "An Improved Equivalence Algorithm",
journal = "Communications of the ACM",
year = "1964",
volume = "7",
pages = "301--303",
}
@Book{ Gamma:design-patterns,
author = "Erich Gamma and Richard Helm and Ralph Johnson and
John Vlissides",
title = "Design Patterns: Elements of Reusable Object-Oriented
Software",
publisher = "Addison Wesley",
address = "Reading, Massachusetts",
year = "1995",
ISBN = "0-201-63361-2",
}
@InProceedings{ GanapathiFischer82,
author = "Ganapathi, M. and Fischer, Charles N.",
title = "Description-Driven Code Generation using Attribute Grammars",
booktitle = "{\popl{9th}}",
year = "1982",
pages = "108--119",
}
@InProceedings{ GandheVenkateshSanyal95,
author = "Gandhe, Milind and Venkatesh, G. and Sanyal, Amitabha",
title = "Labeled {$\lambda$}-calculus and a generalised notion
of strictness",
booktitle = "Asian Computing Science Conference",
series = "Lecture Notes in Computer Science",
month = "December",
publisher = "Springer-Verlag",
year = "1995",
}
@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}
}
@inproceedings{ GanzSabryTaha:ICFP01,
author = {Steven E. Ganz and Amr Sabry and Walid Taha},
title = {Macros as multi-stage computations: type-safe, generative,
binding macros in {MacroML}},
booktitle = icfp,
year = {2001},
isbn = {1-58113-415-0},
pages = {74--85},
location = {Florence, Italy},
doi = {http://doi.acm.org/10.1145/507635.507646},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@Article{ GasserNielsonNielson97,
author = "Kirsten L. Solberg Gasser and Flemming Nielson and
Hanne Riis Nielson",
title = "Systematic realisation of control flow analyses for
{CML}",
journal = "ACM SIG{\-}PLAN Notices",
volume = "32",
number = "8",
pages = "38--51",
month = aug,
year = "1997",
coden = "SINODQ",
ISSN = "0362-1340",
bibdate = "Fri Oct 10 17:39:26 MDT 1997",
acknowledgement = ack-nhfb,
}
@TechReport{ Gaudel78,
author = "Gaudel, Marie-Claude",
title = "Sp\'ecifications Incompl\`etes Mais Suffisantes de la Repr\'esentation des Types Abstraits",
institution = "IRIA",
year = "1978",
type = "Research Report",
number = "320",
month = aug,
}
@Article{ GeschkeMorrisSatterthwaite77,
author = "Geschke, C. M. and Morris, J. H. and Satterthwaite, E. H.",
title = "Early Experience with Mesa",
journal = "Communications of the ACM",
year = "1977",
volume = "20",
pages = "540--553",
}
@InProceedings{ GiacaloneMishraPrasad90,
author = "Alessandro Giacalone and Prateek Mishra and Sanjiva Prasad",
title = "Operational and Algebraic Semantics for Facile: A
Symmetric Integration of Concurrent and Functional Programming",
booktitle = "Proc.\ ICALP '90",
year = "1990",
pages = "765-7780",
publisher = springer,
address = springeraddr,
series = lncs,
volume = 443
}
@InCollection{ GiarratanaGimonaMontanari76,
author = "Giarratana, V. and Gimona, F. and Montanari, U.",
title = "Observability Concepts in Abstract Data Type Specifications",
booktitle = {\mfcs{1976}},
publisher = Springer,
year = "1976",
editor = "A. Mazurkie\-wicz",
series = lncs,
pages = "576--587",
volume = "45",
address = "Berlin, Heidelberg, New York",
}
@PhDThesis{ Ginali76,
author = "Ginali, Susanna",
title = "Iterative Algebraic Theories, Infinite Trees, and Program Schemata",
school = "University of Chicago",
year = "1976",
}
@PhDThesis{ Gladstein94,
author = "David Gladstein",
title = "Compiler Correctness for Concurrent Languages",
school = "Northeastern University",
year = "1994",
address = "Boston, MA",
OPTmonth = dec,
OPTnote = ""
}
@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}
}
@InProceedings{ GlanvilleGraham78,
author = "Glanville, R. S. and Graham, Susan L.",
title = "A New Method for Compiler Code Generation",
booktitle = "{\popl{5th}}",
year = "1978",
}
@Article{ Goguen72,
author = "Goguen, Joseph A.",
title = "Realization is Universal",
journal = "Mathematical Systems Theory",
year = "1972",
volume = "6",
pages = "359--374",
}
@Article{ Goguen74,
author = "Goguen, Joseph A.",
title = "On Homomorphisms, Correctness, Termination,
Unfoldments, and Equiva\-lence of Flow Diagram Programs",
journal = "Journal of Computer and Systems Science",
year = "1974",
volume = "8",
pages = "333--365",
}
@InCollection{ Goguen75,
author = "Goguen, Joseph A.",
title = "Semantics of Computation",
booktitle = "Category Theory Applied to Computation and Control",
publisher = Springer,
year = "1975",
editor = "E. Manes",
series = lncs,
pages = "151--163",
volume = "25",
address = "Berlin, Heidelberg, New York",
}
@InCollection{ Goguen76,
author = "Goguen, Joseph A.",
title = "Correctness and Equivalence of Data Types (Udine, 1975)",
booktitle = "Mathematical Systems Theory",
publisher = Springer,
year = "1976",
editor = "G. Marchesihi and S. K. Mitter",
series = "Lecture Notes in Economics and Mathematical Systems",
pages = "352--358",
volume = "131",
address = "Berlin, Heidelberg, New York",
}
@InCollection{ Goguen78,
author = "Goguen, Joseph A.",
title = "Abstract Errors for Abstract Data Types",
booktitle = "Formal Description of Program\-ming Language Concepts",
publisher = "North-Holland",
year = "1978",
editor = "E. J. Neuhold",
pages = "491--526",
address = "Amsterdam",
}
@TechReport{ GoguenEtAl73,
author = "Goguen, Joseph A. and Thatcher, James W. and Wagner,
Eric G. and Wright, Jesse B.",
title = "A Junction between Computer Science and Category Theory: I,
Basic Definitions and Examples",
institution = "IBM",
year = "1973 and 1976",
note = "Part 1, IBM Research Report RC 4526 (1973);
Part 2, IBM Research Report RC 5908 (1976)"
}
@TechReport{ GoguenEtAl75a,
author = "Goguen, Joseph A. and Thatcher, James W. and Wagner,
Eric G. and Wright, Jesse B.",
title = "An Introduction to Categories, Algebraic Theories, and
Algebras",
institution = "IBM",
year = "1975",
type = "Research Report",
number = "RC 5369",
month = apr,
}
@InProceedings{ GoguenEtAl75b,
author = "Goguen, Joseph A. and Thatcher, James W. and Wagner,
Eric G. and Wright, Jesse B.",
title = "Abstract Data Types as Initial Algebras and Correctness of
Data Representations",
booktitle = "Proceedings on Computer Graphics, Pattern
Recognition, and Data Structures",
year = "1975",
pages = "89--93",
month = may,
}
@InCollection{ GoguenEtAl76,
author = "Goguen, Joseph A. and Thatcher, James W. and Wagner,
Eric G. and Wright, Jesse B.",
title = "Some Fundamentals of Order-Algebraic Semantics",
booktitle = {\mfcs{1976}},
publisher = Springer,
year = "1976",
series = lncs,
volume = "45",
pages = "153--168",
address = "Berlin, Heidelberg, New York",
}
@Article{ GoguenEtAl77,
author = "Goguen, Joseph A. and Thatcher, James W. and Wagner,
Eric G. and Wright, Jesse B.",
title = "Initial Algebra Semantics and Continuous Algebras",
journal = "Journal of the ACM",
year = "1977",
volume = "24",
pages = "68--95",
}
@Unpublished{ GoguenNourani78?,
author = "Goguen, Joseph A. and Nourani, Farshid",
title = "Some Algebraic Techniques for Proving Correctness of Data Type Implementations",
note = "undated extended abstract",
year = "1978??",
}
@InCollection{ GoguenThatcherWagner78,
author = "Goguen, Joseph A. and Thatcher, James W. and Wagner, Eric G.",
title = "An Initial Algebra Approach to the Specification,
Correctness, and Implementation of Abstract Data Types",
booktitle = "Current Trends in Programming Methodology, IV: Data Structuring",
publisher = "Prentice-Hall",
year = "1978",
editor = "R. Yeh",
pages = "80--149",
address = "New Jersey",
}
@InProceedings{ Goldberg91,
author = "Goldberg, Ben",
title = "Tag-Free Garbage Collection for Strongly Typed Programming
Languages",
booktitle = "Proceedings ACM SIGPLAN '91 Symposium on Programming
Language Design and Implementation",
year = "1991",
pages = "165--176",
month = jun,
}
@Book{ GoldbergRobson83,
author = "Goldberg, A. and Robson, D.",
title = "Smalltalk-80: The Language and its Implementation",
publisher = "Addison-Wesley",
year = "1983",
address = "Reading, MA",
}
@InProceedings{ Gomard90,
author = "Gomard, Carsten K.",
title = "Partial Type Inference for Untyped Functional Programs",
booktitle = "{\lfp{1990}}",
year = "1990",
pages = "282--287",
}
@Article{ Gomard92,
author = "Carsten K. Gomard",
title = "A Self-Applicable Partial Evaluator for the Lambda
Calculus: Correctness and Pragmatics",
journal = toplas,
year = "1992",
volume = "14",
number = "2",
pages = "147--172",
}
@Book{ Gordon79,
author = "Gordon, Michael J. C.",
title = "The Denotational Description of
Programming Languages",
publisher = Springer,
year = "1979",
address = "Berlin, Heidelberg, New York",
}
@Book{ Gordon94,
author = "Andrew D. Gordon",
title = "Functional Programming and Input/Output",
publisher = "Cambridge University Press",
year = "1994",
OPTeditor = "",
OPTvolume = "",
OPTseries = "",
address = "Cambridge",
OPTedition = "",
OPTmonth = "",
OPTnote = ""
}
@InProceedings{ Gordon95,
author = "Andrew D. Gordon",
title = "Bisimilarity as a Theory of Functional Programming",
booktitle = "Proceedings of 11th Conference on Mathematical
Foundations of Programming Semantics",
year = "1995",
OPTseries= {Electronic Notes in Theoretical Computer Science},
OPTpublisher={Elsevier Science Publishers B.V.},
OPTvolume=1,
OPTnote="Available at http://www.elsevier.nl/mcs/tcs/pc/vol\-ume1.htm"
}
@inproceedings{Gordon95,
author = "Andrew Gordon",
title = "{A} Tutorial on Co-induction and Functional
Programming",
booktitle = "Functional Programming, Glasgow 1994",
publisher = "Springer Workshops in Computing",
pages = "78--95",
year = "1995",
url = "citeseer.ist.psu.edu/gordon94tutorial.html"
}
@InProceedings{ GordonEtAl78,
author = "Gordon, Michael and Milner, R. and Morris, Lockwood
and Newey, Malcolm and Wadsworth, Christopher",
title = "A Metalanguage for Interactive Proof in {LCF}",
booktitle = "{\popl{5th}}",
year = "1978",
pages = "119--130",
}
GuttmanSwarupRamsdell93 is now GuttmanSwarupRamsdell95
@Book{ GordonMelham93,
author = "Michael J. C. Gordon and T. F. Melham",
title = "Introduction to {HOL}: A Theorem Proving Environment
for Higher-Order Logic",
publisher = "Cambridge University Press",
year = "1993",
OPTeditor = "",
OPTvolume = "",
OPTseries = "",
address = "Cambridge",
OPTedition = "",
OPTmonth = "",
OPTnote = ""
}
@TechReport{ GordonMilnerWadsworth77,
author = "Gordon, Michael and Milner, R. and Wadsworth, Christopher",
title = "Edinburgh {LCF}",
institution = "University of Edinburgh, Department of Computer Science",
year = "1977",
type = "Internal Report",
number = "CSR-11-77",
month = sep,
}
@Book{ Gratzer68,
author = "Gratzer, G.",
title = "Universal Algebra",
publisher = "Van Nostrand",
year = "1968",
address = "Princeton",
}
@Book{ GriswoldPoagePolonsky71,
author = "Griswold, R. E. and Poage, J. F. and Polonsky, I. P.",
title = "The SNOBOL 4 Programming Language",
publisher = "Prentice-Hall",
year = "1971",
address = "Englewood Cliffs, NJ",
edition = "Second",
}
@book{ Gunter-Mitchell94,
editor = "C. A. Gunter and J. C. Mitchell",
title = "Theoretical Aspects of Object-Oriented Programming:
Types, Semantics, and Language Design",
year = "1994",
publisher = "The {MIT} Press"}
@Book{ Gunter92,
author = "Carl A. Gunter",
title = "Semantics of Programming Languages: Structures and
Techniques ",
publisher = "MIT Press",
year = "1992",
address = "Cambridge, MA",
OPTedition = "",
OPTmonth = "",
OPTnote = ""
}
@TechReport{ Guttag75,
author = "Guttag, John V.",
title = "The Specification and Application to
Programming of Abstract Data Types",
institution = "University of Toronto, Department of
Computer Science",
year = "1975",
type = "Computer System Research Report",
number = "CSRG-59",
}
==== H ====
@Article{ Guttag77,
author = "Guttag, John V.",
title = "Abstract Data Types and the Development of Data
Structures",
journal = "Communications of the ACM",
year = "1977",
volume = "20",
pages = "396--404",
}
John Hannan and Dale Miller. From oeprational semantics to abstract
machines: Preliminary results. In Proceedings of the
SIGPLAN Conference on Lisp and Functional
Programming, pages 323--332, 1990.
@Article{ GuttagHorning78,
author = "Guttag, John V. and Horning, James J.",
title = "The Algebraic Specification of Abstract Data Types",
journal = "Acta Informatica",
year = "1978",
volume = "10",
pages = "27--52",
}
@Article{ GuttagHorowitzMusser76,
author = "Guttag, John V. and Horowitz, Ellis and Musser, David R.",
title = "Abstract Data Types and Software Valida\-tion",
journal = "Communications of the ACM",
year = "1978",
volume = "21",
pages = "1048--1064",
}
@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},
}
@Article{ GuttmanSwarupRamsdell95,
author = "J. D. Guttman and V. Swarup and J. Ramsdell",
title = "The {VLISP} Verified Scheme System",
journal = "Lisp and Symbolic Computation",
volume = 8,
number = "1/2",
year = 1995,
pages = "33-110",
}
@Book{ GuttmanWand95,
title = "VLISP: A Verified Implementation of Scheme",
publisher = "Kluwer",
year = 1995,
editor = "Joshua D. Guttman and Mitchell Wand",
address = "Boston",
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",
}
@InProceedings{ HalpernMeyerTrakhtenbrot84,
author = "Halpern, J. Y. and Meyer, Albert R. and Trakhtenbrot, Boris A.",
title = "The Semantics of Local Storage, or What Makes the Free-List Free?",
booktitle = "{\popl{11th}}",
year = "1984",
pages = "245--257",
}
@InCollection{ Hannan91,
author = "Hannan, John",
title = "Making Abstract Machines Less Abstract",
booktitle = "Functional Programming Languages and Computer Architecture, 5th ACM Conference",
year = "1991",
editor = "J. Hughes",
pages = "618--635",
series = lncs,
publisher = springer,
address = springeraddr,
volume = "523",
}
@inproceedings{ Hannan92,
AUTHOR = "John Hannan and Frank Pfenning",
TITLE = "Compiler Verification in {LF}",
BOOKTITLE = "Proceedings of the Seventh Annual IEEE Symposium on
Logic in Computer Science",
EDITOR = "Andre Scedrov",
PUBLISHER = "{IEEE} Computer Society Press",
PAGES = "407--418",
YEAR = 1992}
@InProceedings{ HannanMiller90,
author = {John Hannan and Dale Miller},
title = {From operational semantics to abstract machines:
Preliminary results},
booktitle = lfp90,
year = 1990,
pages = {323-332}
}
Simon Peyton Jones et al. Haskell 98 -- A non-strict, purely functional language. Available from http://www.haskell.org/onlinereport/, February 1999.
@InProceedings{ HarelMeyerPratt77,
author = "Harel, David and Meyer, Albert R. and Pratt, Vaughn R.",
title = "Computability and Completeness in Logics of Programs",
booktitle = "Conference Record 9th Annual ACM Symposium on Theory of Computing",
year = "1977",
pages = "261--268",
}
@InProceedings{ HarelPratt78,
author = "Harel, David and Pratt, Vaughn R.",
title = "Nondeterminism in Logics
of Programs",
booktitle = "{\popl{5th}}",
year = "1978",
pages = "203--213",
}
@InProceedings{ HarperHonsellPlotkin87,
author = "Harper, Robert and Honsell, Furio and Plotkin, Gordon",
title = "A Framework for Defining Logics",
booktitle = {\lics{2nd}},
year = "1987",
pages = "194--204",
}
@Article{ HarperHonsellPlotkin93,
author = "Harper, Robert and Honsell, Furio and Plotkin, Gordon",
title = "A Framework for Defining Logics",
journal = JACM,
year = 1993,
volume = 40,
number = 1,
pages = "143--184",
note = "preliminary version appeared in {\lics{2nd}}, 1987, 194--204."
}
@InProceedings{ Harrison77,
author = "Harrison, William",
title = "A New Strategy for Code Generation --- The General Purpose Optimizing Compiler",
booktitle = "{\popl{4th}}",
year = "1977",
pages = "29--37",
}
@InCollection{ HarrisonOssher93,
key = "Harrison \& Ossher",
author = "William Harrison and Harold Ossher",
title = "Subject-Oriented Programming ({A} Critique of Pure
Objects)",
booktitle = oopsla,
publisher = "ACM Press",
address = "New York",
year = "1993",
editor = "Andreas Paepcke",
OPTvolume = "28",
OPTnumber = "10",
OPTseries = "ACM SIGPLAN Notices",
pages = "411--428",
month = oct,
annote = "Subjectivity. 24 references.",
}
@Misc{ Haskell98Report,
OPTkey = {},
author = {Peyton Jones, Simon and others},
title = {Haskell 98 -- A non-strict, purely functional language},
howpublished = {Available from http://www.haskell.org/onlinereport},
year = {1999},
month = feb,
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@article{ HatcliffDanvy97:mscs,
author = "John Hatcliff and Olivier Danvy",
title = "A Computational Formalization for Partial Evaluation",
journal = "Mathematical Structures in Computer Science",
volume = "7",
number = "5",
pages = "507-541",
year = "1997",
url = "citeseer.nj.nec.com/hatcliff96computational.html" }
@TechReport{ Haynes82,
author = "Haynes, Christopher T.",
title = "A Theory of Data Type Representation Independence",
institution = "University of Iowa Computer Science Department",
year = "1982",
type = "Technical Report",
number = "82-04",
month = dec,
}
@InCollection{ Haynes84,
author = "Haynes, Christopher T.",
title = "Representation Independence for Polymorphic Languages",
booktitle = "Semantics of Data Types: Proceedings",
publisher = Springer,
year = "1984",
editor = "Kahn, Gilles and MacQueen, D. B. and Plotkin, G. D.",
pages = "157--176",
series = lncs,
volume = "173",
address = "Berlin, Heidelberg, New York",
}
@InProceedings{ HaynesFriedman84,
author = "Haynes, Christopher T. and Friedman, Daniel P.",
title = "Engines Build Process Abstractions",
booktitle = "{\lfp{1984}}",
year = "1984",
pages = "18--24",
}
@Article{ HaynesFriedmanWand86,
author = "Haynes, Christopher T. and Friedman, Daniel P. and Wand, Mitchell",
title = "Obtaining coroutines with continuations",
journal = "Computer Languages",
year = "1986",
volume = "11",
number = "3/4",
pages = "143--153",
}
@PhDThesis{ Heintze92,
author = "Nevin Heintze",
title = "Set-Based Program Analysis",
school = "Carnegie-Mellon University",
year = "1992",
address = "Pittsburgh, PA",
OPTmonth = oct,
OPTnote = ""
}
@InProceedings{ Heintze95,
author = {Nevin Heintze},
title = {Control-Flow Analysis and Type Systems},
booktitle = {Static Analysis Symposium},
year = 1995,
pages = {189-206}
}
@InProceedings{ HeintzeJaffar90,
author = {Nevin Heintze and J. Jaffar},
title = {A Decision Procedure for a Class of Set Constraints},
booktitle = lics90,
year = 1990,
organization = {IEEE},
pages = {42-51}
}
@InProceedings{ HeintzeMcAllester97,
author = {Nevin Heintze and David McAllester},
title = {Linear-time Subtransitive Control Flow Analysis},
booktitle = pldi97,
year = 1997,
organization = {ACM},
month = jun,
pages = {261-272}
}
@Book{ Henderson80,
author = "Henderson, Peter",
title = "Functional Programming: Application and Implementation",
publisher = "Prentice-Hall International",
year = "1980",
address = "Englewood Cliffs, NJ",
}
@InProceedings{ HendersonMorris76,
author = "Henderson, Peter and Morris, Jr., James H.",
title = "A Lazy Evaluator",
booktitle = "{\popl{3rd}}",
year = "1976",
pages = "95--103",
}
@InCollection{ Henglein91,
author = "Henglein, Fritz",
title = "Efficient Type Inference for Higher-Order Binding-Time
Analysis",
booktitle = "Functional Programming Languages and Computer Architecture,
5th ACM Conference",
publisher = Springer,
year = "1991",
editor = "J. Hughes",
pages = "448--472",
series = lncs,
volume = "523",
address = "Berlin, Heidelberg, New York",
}
@Article{ Henkin71,
author = "Henkin, Leon",
title = "Mathematical Foundations for Mathematics",
journal = "American Mathematical Monthly",
year = "1971",
volume = "78",
pages = "463--487",
}
@book{ Hennessy:book88,
author = {Matthew Hennessy},
title = {Algebraic theory of processes},
year = {1988},
isbn = {0-262-08171-7},
publisher = {MIT Press},
address = {Cambridge, MA, USA},
}
@InProceedings{ HennessyAshcroft77,
author = "Hennessy, Michael C. B. and Ashcroft, Edward A.",
title = "Parameter-Passing Mechanisms and Nondetermin\-ism",
booktitle = "Proceedings 9th ACM Symposium on Theory of Computing",
year = "1977",
pages = "306--311",
}
@inproceedings{ HennessyMilner80,
author = {Matthew Hennessy and
Robin Milner},
title = {On Observing Nondeterminism and Concurrency.},
booktitle = {ICALP},
year = {1980},
pages = {299-309},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@Article{ HennessyMilner85,
author = "Matthew Hennessy and Robin Milner",
title = "Algebraic Laws for Nondeterminism and Concurrency",
journal = jacm,
year = "1985",
volume = "32",
OPTnumber = "",
pages = "137-161",
OPTmonth = "",
OPTnote = ""
}
@Book{ Herstein64,
author = "Herstein, I. N.",
title = "Topics in Algebra",
publisher = "Blaisdell",
year = "1964",
address = "Waltham, MA",
}
@Article{ Hewitt77,
author = "Hewitt, Carl",
title = "Viewing Control Structures as Patterns of Passing Messages",
journal = "Artificial Intelligence",
year = "1977",
volume = "8",
pages = "323--364",
}
@InProceedings{ HewittEtAl73,
author = "Hewitt, Carl and Bishop, P. and Steiger, R.",
title = "A Universal Modular ACTOR Formalism for Artificial Intelligence",
booktitle = "Proceedings 3rd International Joint Conference on Artificial Intelligence",
year = "1973",
pages = "235--245",
}
@Article{ HewittSmith75,
author = "Hewitt, Carl and Smith, B.",
title = "Towards a Programming Apprentice",
journal = "IEEE Transactions on Software Engineering",
year = "1975",
volume = "SE-1",
pages = "26--45",
}
@Article{ Hindley69,
author = "Hindley, R.",
title = "The Principal Type-Scheme of an Object in Combinatory Logic",
journal = "Transactions of the American Mathematical Society",
year = "1969",
volume = "146",
pages = "29--60",
}
@Article{ Hindley83a,
author = "Hindley, R.",
title = "The Completeness Theorem for Typing $\lambda$-Terms",
journal = "Theoretical Computer Science",
year = "1983",
volume = "22",
pages = "1--17",
}
@Article{ Hindley83b,
author = "Hindley, R.",
title = "Curry's Type-rules are Complete with Respect
to the F-Semantics Too",
journal = "Theoretical Computer Science",
year = "1983",
volume = "22",
pages = "127-133",
}
@InProceedings{ Hinze00,
author = "Ralf Hinze",
title = "Deriving backtracking monad transformers.",
pages = "186--197",
booktitle = icfp,
year = "2000",
}
@Article{ Hoare69,
author = "Hoare, C. A. R.",
title = "An Axiomatic Basis for Computer Programming",
journal = "Communications of the ACM",
year = "1969",
volume = "12",
pages = "576--580, 583",
}
@Article{ Hoare72,
author = "Hoare, C. A. R.",
title = "Proving Correctness of Data Representations",
journal = "Acta Informatica",
year = "1972",
volume = "1",
pages = "271--281",
}
@Article{ Hoare74,
author = "Hoare, C. A. R.",
title = "Monitors: an Operating System Structuring Concept",
journal = "Communications of the ACM",
year = "1974",
volume = "17",
pages = "549--557",
}
@Article{ Hoare78,
author = "Hoare, C. A. R.",
title = "Communicating Sequential Processes",
journal = "Communications of the ACM",
year = "1978",
volume = "21",
pages = "666--677",
}
@Article{ HoareLauer74,
author = "Hoare, C. A. R. and Lauer, Peter",
title = "Consistent and Complementary Formal Theories of the Semantics of Programming Languages",
journal = "Acta Informatica",
year = "1974",
volume = "3",
pages = "135--153",
}
@Article{ Hoffman78,
author = "Hoffman, Christopher M.",
title = "Design and Correctness of a Compiler for a
Non-Procedural Language",
journal = "Acta Informatica",
year = "1978",
volume = "9",
pages = "217--241",
}
@TechReport{ HoffmanPierce92,
author = "Martin Hoffman and Benjamin Pierce",
title = "An Abstract View of Objects and Subtyping",
institution = "University of Edinburgh, Department of
Computer Science",
year = 1992,
OPTtype = "",
number = "ECS-LFCS-92-226",
OPTaddress = "",
month = aug,
OPTnote = ""
}
@Book{ Hofstadter79,
author = "Hofstadter, Douglas R.",
title = "G{\"o}del, Escher, Bach: An Eternal Golden Braid",
publisher = "Basic Books",
year = "1979",
address = "New York",
}
@TechReport{ HollowayEtAl79,
author = "Holloway, J. and Steele, Guy L. and Sussman, Gerald Jay and Bell, A.",
title = "The SCHEME-79 Chip",
institution = "MIT Artificial Intelligence Laboratory",
year = "1979",
type = "Memo",
number = "559",
month = dec,
}
@InProceedings{ HondaBergerYoshida:lics05,
author = {Kohei Honda and Martin Berger and Nobuko Yoshida},
title = {An Observationally Complete Program Logic for Imperative
Higher-Order Functions},
booktitle = {Proceedings of the Twentieth Annual IEEE Symposium on
Logic in Computer Science ({LICS})},
pages = {280-293},
year = {2005},
month = {June},
URL = {http://www.dcs.qmul.ac.uk/%7Ekohei/logics/imperative1short.ps}
}
@Article{ Honselletal95,
author = "Furio Honsell and Ian A. Mason and Scott Smith and
Carolyn Talcott",
title = "A Variable Typed Logic of Effects",
journal = "Information and Computation",
year = "1995",
volume = "119",
OPTnumber = "",
pages = "55-90",
OPTmonth = "",
OPTnote = ""
}
@InCollection{ Hook84,
author = "Hook, James G.",
title = "Understanding Russell: A First Attempt",
booktitle = "Semantics of Data Types: Proceedings",
publisher = Springer,
year = "1984",
editor = "Kahn, Gilles and MacQueen, David B. and Plotkin, Gordon D.",
pages = "69--86",
series = lncs,
volume = "173",
address = "Berlin, Heidelberg, New York",
}
@Book{ HorowitzSahni76,
author = "Horowitz, Ellis and Sahni, Sartaj",
title = " Fundamentals of Data Structures",
publisher = "Compu\-ter Science Press",
year = "1976",
address = "Woodland Hills, CA",
}
@Article{ HorwitzRepsBinkley84,
author = "Horwitz, Susan and Reps, Thomas and Binkley, David",
title = "Program Slicing",
journal = "IEEE Transactions on Software Engineering",
volume = "10",
number = "4",
pages = "352--357",
month = "August",
year = 1984}
@InProceedings{ Howe89,
author = "Douglas J. Howe",
title = "Equality in Lazy Computation Systems",
booktitle = lics89,
year = "1989",
pages = "198-203",
}
@Article{ Howe94,
author = {Douglas J. Howe},
title = {Proving Congruence of Bisimulation in Functional
Programming Languages},
journal = ic,
year = 1996,
volume = {124},
number = {2},
month = feb,
pages = {103-112},
}
@Unpublished{ Howe95,
author = "Douglas J. Howe",
title = "A Note on Proving Congruence of Bisimulation in a
Generalized Lambda Calculus",
note = "unpublished manuscript",
year = "1995",
OPTmonth = ""
}
@InProceedings{ Hudak86,
author = {Paul Hudak},
title = {A semantic model of reference counting and its
abstraction },
booktitle = lfp86,
year = 1986,
organization = {ACM},
pages = {351-363}
}
@InProceedings{ HudakBloss85,
author = {Paul Hudak and Adrienne Bloss},
title = {Avoiding Copying in Functional and Logic Programming
Languages},
booktitle = popl12,
year = 1985,
organization = {ACM},
pages = {300-314}
}
@InProceedings{ Hughes82,
author = "Hughes, R. J. M.",
title = "Super Combinators: A New Implementation Method for
Applicative Languages",
booktitle = "{\lfp{1982}}",
year = "1982",
pages = "1--10",
}
@incollection{ Hughes95,
author = "Hughes, John",
title = "The Design of a Pretty-printing Library",
booktitle = "Advanced Functional Programming",
volume = "925",
publisher = "Springer Verlag",
editor = "Jeuring, J. and Meijer, E.",
year = "1995",
url = "citeseer.nj.nec.com/hughes95design.html" }
@InProceedings{ HuntSands91,
author = "Sebastian Hunt and David Sands",
title = "Binding Time Analysis: A New PERspective",
booktitle = "Proceedings of the Symposium on Partial Evaluation
and Semantics-Based Program Manipulation",
year = "1991",
pages = "154-165",
note = "SIGPLAN Notices 26(9), September, 1991"
}
@Proceedings{ ICRS75,
key = "International Conference on Reliable Software",
title = "Proceedings - 1975 International Conference on
Reliable Software",
year = "1975",
note = "{\it SIGPLAN Notices}, 10(6), June 1975"
}
@Manual{ IEEE91,
title = "{IEEE} Standard for the Scheme Programming Language,
{IEEE} Standard 1178-1990",
organization = "IEEE Computer Society",
address = "New York",
year = "1991",
}
@inproceedings{ Igarashi-etal99:Featherweight-Java,
author = "Atshushi Igarashi and Benjamin Pierce and Philip Wadler",
title = "{Featherweight Java}: {A} Minimal Core Calculus for {Java} and {GJ}",
booktitle = "Proceedings of the 1999 {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages {\&} Applications ({OOPSLA}`99)",
volume = "34(10)",
address = "N. Y.",
editor = "Loren Meissner",
pages = "132--146",
year = "1999",
url = "citeseer.nj.nec.com/igarashi99featherweight.html" }
@InProceedings{ Ingalls78,
author = "Ingalls, D.",
title = "The Smalltalk-76 Programming System",
booktitle = "{\popl{5th}}",
year = "1978",
pages = "9--16",
}
@Article{ JMorris73,
author = "Morris, Jr., James H.",
title = "Protection in Programming Languages",
journal = "Communications of the ACM",
year = "1973",
volume = "16",
pages = "15--21",
}
@article{ JacobsRutten97,
author = "Bart Jacobs and Jan Rutten",
title = "A Tutorial on (Co)Algebras and (Co)Induction",
journal = "Bulletin of the European Association for Theoretical
Computer Science",
volume = "62",
pages = "222--259",
year = "1997",
url = "citeseer.ist.psu.edu/jacobs97tutorial.html"
}
@InProceedings{ JagadeesanJeffreyRiely:ecoop03,
author = {R. Jagadeesan and A. S. A. Jeffrey and J. Riely},
title = {A Calculus of Untyped Aspect-Oriented Programs},
booktitle = ecoop,
pages = {415--427},
year = {2003},
volume = {1853},
series = lncs,
publisher = springer,
address = springeraddr,
url = {http://cm.bell-labs.com/who/ajeffrey/papers/ecoop03.pdf}
}
@Article{ James78,
author = "James, J. S.",
title = "FORTH for Microcomputers",
journal = "SIGPLAN Notices",
year = "1978",
volume = "13",
number = "10",
pages = "33--39",
month = oct,
}
@InCollection{ JanssenvanEmdeBoas77a,
author = "Janssen, T. H. V. and van Emde Boas, P.",
title = "On the Proper Treatment of Referencing, Dereferencing, and Assignment",
booktitle = "Proceedings 4th International Conference on Automata, Languages, and Programming",
publisher = Springer,
year = "1977",
series = lncs,
address = "Berlin, Heidelberg, New York",
}
@InCollection{ JanssenvanEmdeBoas77b,
author = "Janssen, T. H. V. and van Emde Boas, P.",
title = "The Expressive Power of Intensional Logic in the Semantics of Programming Languages",
booktitle = {\mfcs{1977}},
year = "1977",
editor = "J. Gruska",
pages = "303--311",
series = lncs,
volume = "53",
publisher = springer,
address = springeraddr,
}
@InProceedings{ JategaonkarMitchell88,
author = "Jategaonkar, Lalita A. and Mitchell, John C.",
title = "ML with Extended Pattern Matching and Subtypes",
booktitle = "{\lfp{1988}}",
year = "1988",
pages = "198--211",
}
@Article{ JeffersonFriedman96,
author = {Stanley Jefferson and Daniel P. Friedman},
title = {A Simple Reflective Interpreter},
journal = {Lisp and Symbolic Computation},
year = {1996},
OPTkey = {},
volume = {9},
number = {2/3},
month = {May/June},
pages = {181-202},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@InProceedings{ JeffreyRathke-esop05,
author = {A. S. A. Jeffrey and J. Rathke},
title = {Java Jr.: Fully Abstract Trace Semantics for a Core {Java} Language},
booktitle = {Proc. European Symposium on Programming},
year = {2005},
pages = {423-438},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {3444},
url = {http://cm.bell-labs.com/who/ajeffrey/papers/esop05.pdf}
}
@TechReport{ JimMeyer91,
author = {Trevor Jim and Albert R. Meyer},
title = {Full Abstraction and the Context Lemma},
institution = {MIT Laboratory for Computer Science},
year = {1991},
OPTkey = {},
OPTtype = {},
number = {MIT/LCS/TR-524},
OPTaddress = {},
month = dec,
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@TechReport{ Johnson75,
author = "Johnson, S. C.",
title = "Yacc: Yet Another Compiler-Compiler",
institution = "Bell Laboratories",
year = "1975",
type = "Technical Report",
number = "CSTR32",
address = "Murray Hill, NJ",
}
@InProceedings{ JohnsonDuggan88,
author = "Johnson, G. F. and Duggan, D.",
title = "Stores and Partial Continuations as First-Class Objects in a Language and its Environment",
booktitle = "{\popl{15th}}",
year = "1988",
}
@InProceedings{ Johnston71,
author = "Johnston, J. B.",
title = "The Contour Model of Block Structured
Processes",
booktitle = "Proceedings ACM Symposium on Data Structures in Programming
Languages",
year = "1971",
note = "{\it SIGPLAN Notices} 6(2):55--81, February 1971"
}
@Book{ Jones80,
title = "Semantics-Directed Compiler Generation",
publisher = Springer,
year = "1980",
editor = "Jones, Neil D.",
volume = "94",
series = lncs,
address = "Berlin, Heidelberg, New York",
}
@InProceedings{ Jones81,
author = "Neil D. Jones",
title = "Flow Analysis of Lambda Expressions",
booktitle = "International Colloquium on Automata, Languages, and
Programming ",
pages = "114-128",
publisher = springer,
series = lncs,
volume = 115,
address = springeraddr,
year = 1981
}
@Article{ Jones95,
title = "A system of constructor classes: overloading and
implicit higher-order polymorphism",
author = "Mark P. Jones",
pages = "1--37",
journal = "Journal of Functional Programming",
month = jan,
year = "1995",
volume = "5",
number = "1",
references = "\cite{JFP::Barendregt1991}
\cite{LICS::Breazu-TannenCGS1989}
\cite{POPL::DamasM1982} \cite{LICS::Moggi1989}
\cite{JACM::Robinson1965}",
}
@Article{ JonesEtAl89,
author = "Jones, Neil D. and Sestoft, Peter and S{\o}ndergaard, Harald",
title = "MIX: A Self-Applicable Partial Evaluator for
Experiments in Compiler Generation",
journal = "Lisp and Symbolic Computation",
year = "1989",
volume = "2",
pages = "9--50",
}
@InProceedings{ JonesMuchnick82,
author = "Neil D. Jones and Steven S. Muchnick",
title = "A Flexible Approach to Interprocedural Data Flow
Analysis and Progrms with Recursive Data Structures",
booktitle = "\popl{9th}",
year = "1982",
pages = "66--74",
}
@InProceedings{ JonesMycroft84,
author = "Jones, Neil D. and Mycroft, Alan",
title = "Stepwise Development
of Operational and Denotational Semantics for Prolog",
booktitle = "1984 International Symposium on Logic Programming",
year = "1984",
address = "Atlantic City",
month = feb,
}
@InCollection{ JonesSchmidt80,
author = "Jones, Neil D. and Schmidt, David A.",
title = "Stepwise Development of Operational and Denotational Semantics for Prolog",
booktitle = "Semantics-Directed Compiler Generation",
publisher = Springer,
year = "1980",
editor = "Jones, Neil D.",
pages = "70--93",
address = "Berlin, Heidelberg, New York",
series = lncs,
volume = "94",
}
@InProceedings{ JorringScherlis86,
author = "Jorring, U. and Scherlis, William L.",
title = "Compilers and Staging Transformations",
booktitle = "{\popl{13th}}",
year = "1986",
pages = "86--96",
}
@InCollection{ KahnCarlsson84,
author = {K. M. Kahn and M. Carlsson},
title = {How to Implement Prolog on a {LISP} Machine},
booktitle = {Implementations of Prolog},
OPTcrossref = {},
OPTkey = {},
pages = {119-134},
OPTpublisher = {Ellis Horwood},
year = {1984},
editor = {J. A. Campbell},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTtype = {},
OPTchapter = {},
address = {Chichester},
OPTedition = {},
OPTmonth = {},
OPTnote = {},
OPTannote = {}
}
@Book{ KahnMacQueenPlotkin84,
title = "Semantics of Data Types: Proceedings",
publisher = Springer,
year = "1984",
editor = "Kahn, Gilles and MacQueen, David B. and Plotkin, Gordon D.",
volume = "173",
series = lncs,
address = "Berlin, Heidelberg, New York",
}
@Book{ KalishMontague64,
author = "Kalish, D. and Montague, R.",
title = "Techniques of Formal Reasoning",
publisher = "Harcourt-Brace",
year = "1964",
address = "New York",
}
@InProceedings{ Kamin80,
author = "Kamin, Samuel",
title = "Final Data Type Specifications: A New Data Type
Specification Method",
booktitle = "{\popl{7th}}",
year = "1980",
pages = "131--138",
}
@InProceedings{ Kamin88,
author = "Kamin, Samuel",
title = "Inheritance in Smalltalk-80: A Denotational
Definition",
booktitle = "{\popl{15th}}",
year = "1988",
pages = "80--87",
}
@InProceedings{ KanellakisMitchell89,
author = "Kanellakis, Paris C. and Mitchell, John C.",
title = "Polymorphic Unification and ML Typing",
booktitle = "{\popl{16th}}",
year = "1989",
}
@Book{ Keene89,
author = "Keene, S.E.",
title = "Object-Oriented Programming in Common Lisp",
publisher = "Addison-Wesley",
year = "1989",
address = "Reading, MA",
}
@Article{ KelseyClingerReesEtAl98,
author = "Richard Kelsey and William Clinger and Jonathan Rees [editors]",
title = "Revised{$^5$} Report on the Algorithmic Language {S}cheme",
journal = "Higher-Order and Symbolic Computation",
volume = "11",
number = "1",
month = "August",
year = "1998",
pages = "7--104",
note = "Also appeared in {\em SIGPLAN Notices} 33:9, September 1998"
}
@InProceedings{ KelseyHudak89,
author = "Kelsey, Richard and Hudak, Paul",
title = "Realistic Compilation by Program Transformation",
booktitle = "{\popl{16th}}",
year = "1989",
pages = "281--292",
}
@InProceedings{ KfouryTiurynUrzycyzn88,
author = "Kfoury, A. J. and Tiuryn, J. and Urzycyzn, P.",
title = "A Proper Extension of ML with an Effective Type-Assignment",
booktitle = "{\popl{15th}}",
year = "1988",
pages = "58--69",
}
@article{ Kiczales-etal:CACM2001:getting-started,
author = {Gregor Kiczales and Erik Hilsdale and Jim Hugunin and Mik Kersten and Jeffrey Palm and William Griswold},
title = {Getting started with ASPECTJ},
journal = {Communications of the ACM},
volume = {44},
number = {10},
year = {2001},
issn = {0001-0782},
pages = {59--65},
doi = {http://doi.acm.org/10.1145/383845.383858},
publisher = {ACM Press},
}
@Book{ Kiczales91:amop,
author = "Gregor Kiczales and Jim des Rivieres",
title = "The art of the metaobject protocol",
publisher = "MIT Press",
address = "Cambridge, MA, USA",
pages = "viii + 335",
year = "1991",
ISBN = "0-262-11158-6 (hardcover), 0-262-61074-4 (paperback)",
LCCN = "QA76.73.C28 K53 1991",
bibdate = "Wed Sep 29 06:22:23 1999",
acknowledgement = ack-nhfb,
keywords = "Common LISP (Computer program language);
Object-oriented programming (Computer science)",
}
@Article{ Kiczales96:ieee-software,
key = "kiczales96a",
author = "Gregor Kiczales",
title = "Beyond the Black Box: Open Implementation",
journal = "IEEE Software",
month = jan,
year = "1996",
volume = "13",
number = "1",
pages = "8--11",
abstract = "Encapsulation, informally known as black-box
abstraction, is a widely known and accepted principle.
It is a basic tenet of software design, underlying
approaches to portability and reuse. However, many
practitioners find themselves violating it in order to
achieve performance requirements in a practical manner.
The gap between theory and practice must be filled.
Open implementation is a controversial new approach
that claims to do just that. The paper provides some
ideas to spark further debate on black-box abstraction
(0 Refs.)",
}
@inproceedings{ Kiczales:ECOOP01,
author = "Gregor Kiczales and Erik Hilsdale and Jim Hugunin and
Mik Kersen and Jeffrey Palm and William G. Griswold",
title = "An Overview of {AspectJ}",
booktitle = ecoop,
pages = "327-353",
volume = 2072,
series = lncs,
year = 2001,
publisher = springer,
address = springeraddr
}
@incollection{ Kiczales:ECOOP97,
author = "Gregor Kiczales and John Lamping and Anurag Mendhekar and Chris Maeda and Cristina Lopes and Jean-Marc Loingtier and John Irwin",
title = "Aspect-Oriented Programming",
booktitle = ecoop,
volume = "1241",
publisher = springer,
address = springeraddr,
editor = "Mehmet Ak\c{s}it and Satoshi Matsuoka",
pages = "220--242",
year = "1997",
url = "citeseer.nj.nec.com/kiczales97aspectoriented.html"
}
@InProceedings{ KiniMartinStoughton82,
author = "Kini, V. and Martin, D. F. and Stoughton, A.",
title = "Testing the INRIA Ada Formal Definition: The USC-ISI
Formal Semantics Project",
booktitle = "Proceedings ADATec Meeting",
year = "1982",
}
@Book{ Kleene52,
author = "Kleene, Stephen C.",
title = "Introduction to Metamathematics",
publisher = "Van Nostrand",
year = "1952",
address = "Princeton, NJ",
}
@Article{ KnoopRuthingSteffen94,
author = "Knoop, James and R{\"{u}}thing, Oliver and Steffen, Bernhard",
title = "Partial dead code elimination",
journal = "SIGPLAN Notices",
volume = "29",
number = "6",
year = "1994",
pages = "147--158",
note = "{\it Proceedings of the ACM SIGPLAN '94 Conference on
Programming Language Design and Implementation}"
}
@Book{ Knuth68a,
author = "Knuth, Donald E.",
title = "The Art of Computer Programming, Vol. I:
Fundamental Algorithms",
publisher = "Addison Wesley",
year = "1968",
address = "Reading, MA",
note = "Second edition, 1973"
}
@Article{ Knuth68b,
author = "Knuth, Donald E.",
title = "Semantics of Context-Free Languages",
journal = "Mathematical Systems Theory",
year = "1968",
volume = "2",
pages = "127--145",
note = "Correction, 5:95-96, 1971"
}
@Article{ Knuth74a,
author = "Knuth, Donald E.",
title = "Structured Programming with go to Statements",
journal = "Computing Surveys",
year = "1974",
volume = "6",
pages = "261--301",
}
@TechReport{ Knuth74b,
author = "Knuth, Donald E.",
title = "An Analysis of Alpha-Beta Pruning",
institution = "Stanford University Computer Science Deptartment",
year = "1974",
type = "Technical Report",
number = "STAN-CS-74-441",
note = "Appeared in {\it Artificial Intelligence}"
}
@InCollection{ KnuthPardo77,
author = "Knuth, Donald E. and Pardo, L. T.",
title = "The Early Development of Programming Languages",
booktitle = "Encyclopedia of Computer Science and Technology",
publisher = "Marcel Dekker",
year = "1977",
editor = "J. Belzer and A. G. Holzman and D. Kent",
pages = "419--493",
address = "New York",
volume = "6",
}
@PhDThesis{ Kohlbecker86,
author = "Kohlbecker, Eugene M.",
title = "Syntactic Extensions in the Programming Language Lisp",
school = "Indiana University",
year = "1986",
address = "Bloomington, IN",
month = aug,
}
@InProceedings{ KohlbeckerEtAl86,
author = "Kohlbecker, Eugene M. and Friedman, Daniel P. and
Felleisen, Matthias and Duba, Bruce",
title = "Hygienic Macro Expansion",
booktitle = "{\lfp{1986}}",
year = "1986",
pages = "151--161",
}
#InProceedings{Lammel01,
author = "Ralf L{\"a}mmel",
title = "{Semantics of Method Call Interception}",
booktitle = "{Workshop Aspekt-Orientierung
der GI-Fachgrupppe 2.1.9 Objektorientiere Software-Entwicklung,
3.- 4. Mai 2001, Universit{\"a}t Paderborn}",
year = "2001",
note = "Technical Report tr-ri-01-223 Universit{\"a}t-Gesamthochschule Paderborn, available at {\tt www.cwi.nl/{\char'176}ralf}"
}
@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",
}
@Article{ KolblWand87,
author = "Kolbl, Stephan and Wand, Mitchell",
title = "Linear Future Semantics and its Implementation",
journal = "Science of Computer Programming",
year = "1987",
volume = "8",
pages = "87--103",
}
@Book{ Korfhage74,
author = "Korfhage, R. R.",
title = "Discrete Computational Structures",
publisher = "Academic Press",
year = "1974",
address = "New York",
}
@InProceedings{ KoutavasWand-esop06,
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,
OPTmonth = {},
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.},
}
@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 \sp 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{ KranzEtAl86,
author = "Kranz, David~A. and Kel\-sey, Richard and Rees, Jona\-than A. and
Hudak, Paul and Philbin, James and Adams, Norman I.",
title = "Orbit: An Optimizing Compiler for Scheme",
booktitle = "Proceedings SIGPLAN '86 Symposium on Compiler Construction",
year = "1986",
note = "{\it {SIGPLAN Notices 21}\/}(7), July, 1986, 219-223"
}
@inproceedings{ KrishnamurthiErlichFelleisen:esop99,
author="Shriram Krishnamurthi and Yan-David Erlich and Matthias
Felleisen",
title="Expressing Structural Properties as Language Constructs",
booktitle=esop,
year=1999,
publisher= springer,
address = springeraddr,
month=mar,
series=lncs,
number=1576,
pages="258--272"}
}
@inproceedings{ KrishnamurthiFelleisenDuba:gcse99,
author="Shriram Krishnamurthi and Matthias Felleisen and Bruce
F.~Duba",
title="From Macros to Reusable Generative Programming",
booktitle=gcse,
year=1999,
month=sep,
publisher = springer,
address = springeraddr,
series=lncs,
pages="105--120",
number=1799}
Functorial Semantics of Algebraic Theories
and
Some Algebraic Problems in the context of
Functorial Semantics of Algebraic Theories
F. William Lawvere
Originally published as:
Ph.D. thesis, Columbia University, 1963
and
in Reports of the Midwest Category Seminar II, 1968, 41-61,
© Springer-Verlag, and used by permission.
The authors comments are © F. William Lawvere, 2004.
Keywords: Algebraic theories, functorial semantics
2000 MSC: 18.10
Republished in:
Reprints in Theory and Applications of Categories, No. 5 (2004) pp 1-121
http://www.tac.mta.ca/tac/reprints/articles/5/tr5.dvi
http://www.tac.mta.ca/tac/reprints/articles/5/tr5.ps
http://www.tac.mta.ca/tac/reprints/articles/5/tr5.pdf
@Article{ KuhnelMeseguerPfenderSols75,
author = "Kuhnel, W. and Meseguer, J. and Pfender, M. and Sols, I.",
title = "Primitive Recursive Algebraic Theories with Applications to
Program Schemes (abstract)",
journal = "Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle",
year = "1975",
volume = "16",
pages = "271--273",
}
@InProceedings{ LMorris73,
author = "Morris, F. Lockwood",
title = "Advice on Structuring Compilers and Proving Them Correct",
booktitle = "{\popl{1st}}",
year = "1973",
pages = "144--152",
address = "Boston",
}
@inproceedings{ Laird-fossacs03,
author = {James Laird},
title = {A Game Semantics of Linearly Used Continuations.},
booktitle = {FoSSaCS},
year = {2003},
pages = {313-327},
ee = {http://link.springer.de/link/service/series/0558/bibs/2620/26200313.htm},
OPTcrossref = {DBLP:conf/fossacs/2003},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InProceedings{ Lammel01,
author = {Ralf L{\"a}mmel},
title = {A Semantical Approach to Method-call Interception},
booktitle = aosd,
OPTcrossref = {},
OPTkey = {},
editor = {Gregor Kiczales},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
year = {2002},
OPTorganization = {},
publisher = {ACM Press},
address = {Enschede, The Netherlands},
month = apr,
OPTpages = {},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@Article{ Landin64,
author = "Landin, Peter J.",
title = "The Mechanical Evaluation of Expressions",
journal = "Computer Journal",
year = "1964",
volume = "6",
pages = "308--320",
}
@Article{ Landin65,
author = "Landin, Peter J.",
title = "A Correspondence Between ALGOL 60 and Church's Lambda-Notation: {Part I}",
journal = "Communications of the ACM",
year = "1965",
volume = "8",
pages = "89--101",
}
@Article{ Landin66,
author = "Landin, Peter J.",
title = "The Next 700 Programming Languages",
journal = "Communications of the ACM",
year = "1966",
volume = "9",
pages = "157--166",
}
@Article{ LangPerlmutter88,
author = "Lang, K. J. and Perlmutter, B. A.",
title = "Oaklisp: An Object-Oriented Dialect of Scheme",
journal = "Lisp and Symbolic Computation",
year = "1988",
volume = "1",
pages = "39--52",
}
@PhDThesis{ Lao86,
author = "Lao, Marek J.",
title = "Applying Wand's Technique to the Problems of
Addressing for Programming Languages with Multilevel Prefixing",
school = "University of Warsaw",
year = "1986",
}
@PhDThesis{ Launchbury89,
author = "John Launchbury",
title = "Projection Factorizations in Partial Evaluation",
school = "University of Glasgow",
year = "1989",
month = nov,
}
@InProceedings{ Launchbury91,
author = "John Launchbury",
title = "A Strongly-Typed Self-Applicable Partial Evaluator",
booktitle = "Functional Programming Languages and Computer Architecture",
year = "1991",
editor = "John Hughes",
pages = "145-164",
publisher = springer,
address = springeraddr,
volume = 523
}
@Article{ Lawvere63,
author = "Lawvere, F. William",
title = "Functorial Semantics of Algebraic Theories",
journal = "Proceedings National Academy of Sciences USA",
year = "1963",
volume = "50",
pages = "869--872",
}
@Book{ Lawvere72,
title = "Toposes, Algebraic Geometry, and Logic",
publisher = Springer,
year = "1972",
editor = "Lawvere, F. William",
volume = "274",
series = lncs,
address = "Berlin, Heidelberg, New York",
}
@InCollection{ LeRoyMauny91,
author = "LeRoy Xavier and Mauny, Michael",
title = "Dynamics in {ML}",
booktitle = "Functional Programming Languages and Computer Architecture, 5th ACM Conference",
publisher = Springer,
year = "1991",
editor = "J. Hughes",
pages = "406--426",
series = lncs,
volume = "523",
address = "Berlin, Heidelberg, New York",
}
@incollection{ LeavensDara00,
author = "Gary T. Leavens and Krishna Kishore Dhara",
title = "Concepts of Behavioral Subtyping and a Sketch of Their Extension to Component-Based Systems",
booktitle = "Foundations of Component-Based Systems",
publisher = "Cambridge University Press",
editor = "Gary T. Leavens and Murali Sitaraman",
pages = "113--135",
year = "2000",
url = "citeseer.ist.psu.edu/leavens00concepts.html" }
#TECHREPORT{LieberherrOrleansOvlinger01,
AUTHOR = "Karl Lieberherr and Doug Orleans and Johan Ovlinger",
TITLE = "{Aspect-Oriented Programming with Aspectual Methods}",
INSTITUTION = "College of Computer Science, Northeastern University",
YEAR = 2001,
MONTH = "February",
NUMBER = "{NU-CCS-2001-01}",
ADDRESS = "Boston, MA",
PAGES = "1-15"
}
@Book{ Lee91,
author = "Lee, Peter",
title = "Topics in Advanced Language Implementation",
publisher = "MIT Press",
year = "1991",
address = "Cambridge, MA",
}
@InProceedings{ LeeEtAl88,
author = "Lee, Peter and Pfenning, Frank and Rollins, Gregory
and Scherlis, William",
title = "The Ergo Support System: An Integrated Set of Tools
for Prototyping Integrated Environments",
booktitle = "Proceedings ACM SIGSOFT/SIGPLAN Software Engineering
Symposium on Practical Software Development Environments",
year = "1988",
pages = "25--34",
month = nov,
}
@InProceedings{ LeePleban86,
author = "Lee, Peter and Pleban, Uwe",
title = "On the Use of {LISP} in Implementing Denotational Semantics",
booktitle = "{\lfp{1986}}",
year = "1986",
pages = "233--248",
}
@TechReport{ LehmannSmyth77,
author = "Lehmann, Daniel J. and Smyth, Michael B.",
title = "Data Types",
institution = "University of Warwick",
year = "1977",
type = "Theory of Compu\-ta\-tion Report",
number = "19",
month = may,
}
@Article{ LehmannSmyth81,
author = "Lehmann, Daniel J. and Smyth, Michael B.",
title = "Algebraic Specification of Data Types: A Synthetic Approach",
journal = "Mathematical Systems Theory",
year = "1981",
volume = "14",
pages = "97--139",
}
@InProceedings{ Leivant83,
author = "Leivant, Daniel",
title = "Structural Semantics for Polymorphic Data Types
(preliminary report)",
booktitle = "{\popl{10th}}",
year = "1983",
pages = "155--166",
}
@InProceedings{ Leroy-popl94,
author = "Xavier Leroy",
title = "Manifest types, modules, and separate compilation",
booktitle = popl21,
year = "1994",
pages = "109--122",
url = "http://www.acm.org:80/pubs/citations/proceedings/plan/174675/p109-leroy/",
abstract = "This paper presents a variant of the SML module system
that introduces a strict distinction between abstract
types and manifest types (types whose definitions are
part of the module specification), while retaining most
of the expressive power of the SML module system. The
resulting module system provides much better support
for separate compilation.",
}
@TechReport{ Leroy90,
author = "Xavier Leroy",
title = "The {ZINC} experiment: an economical implementation of
the {ML} language",
institution = "INRIA",
number = "117",
year = "1991",
}
@inproceedings{ LewisEtal:popl00,
author = {Jeffrey R. Lewis and John Launchbury and Erik Meijer and Mark B. Shields},
title = {Implicit parameters: dynamic scoping with static types},
booktitle = popl27,
year = {2000},
isbn = {1-58113-125-9},
pages = {108--118},
location = {Boston, MA, USA},
doi = {http://doi.acm.org/10.1145/325694.325708},
publisher = {ACM Press},
address = {New York, NY, USA}
}
==== M ====
@Book{ Lewisetal99,
author = "Bil Lewis and Dan LaLiberte and Richard Stallman and
the GNU Manual Group",
title = "{GNU Emacs Lisp} Reference Manual, for {Emacs} Version
20.4",
publisher = "Free Software Foundation",
address = "675 Mass Ave, Cambridge, MA 02139, USA, Tel: (617)
876-3296, USA",
pages = "????",
year = "1999",
ISBN = "1-882114-72-8",
LCCN = "????",
bibdate = "Wed Sep 20 10:36:28 2000",
acknowledgement = ack-nhfb,
}
@inproceedings{ LiangHudakJones:popl95,
author = "Sheng Liang and Paul Hudak and Mark Jones",
title = "Monad transformers and modular interpreters",
booktitle = "{\popl{22nd}}",
publisher = "ACM Press",
address = "New York, NY, USA",
editor = "{ACM}",
isbn = "0-89791-692-1",
pages = "333--343",
year = "1995",
url = "citeseer.nj.nec.com/liang95monad.html" }
@book{ Lieberherr96:book,
author = "K. J. Lieberherr",
title = "Adaptive Object-Oriented Software: The {D}emeter {M}ethod with Propagation Patterns",
publisher = "PWS Publishing Company",
address = {Boston, Mass.},
year = "1996",
url = "citeseer.nj.nec.com/lieberherr96adaptive.html"
}
@article{ LieberherrOrleansOvlinger01,
author = {Karl Lieberherr and Doug Orleans and Johan Ovlinger},
title = {Aspect-oriented programming with adaptive methods},
journal = {Communications of the ACM},
volume = {44},
number = {10},
year = {2001},
issn = {0001-0782},
pages = {39--41},
doi = {http://doi.acm.org/10.1145/383845.383855},
publisher = {ACM Press},
}
@Article{ Lipton75,
author = "Lipton, Robert J.",
title = "Reduction: A Method of Proving Properties of
Parallel Programs",
journal = "Communications of the ACM",
year = "1975",
volume = "18",
pages = "717--721",
}
@TechReport{ LiptonSnyder77,
author = "Lipton, Robert J. and Snyder, Lawrence",
title = "On the Halting of Tree Replacement Systems",
institution = "Yale University Department of Computer Science",
year = "1977",
type = "Research Report",
number = "99",
address = "New Haven, CT",
}
@Article{ LiskovEtAl77,
author = "Liskov, Barbara and Snyder, Alan and Atkinson, R. and
Schaffert, Craig",
title = "Abstraction Mechanisms in {CLU}",
journal = "Communications of the ACM",
year = "1977",
volume = "20",
pages = "564--576",
}
@Article{ LiskovZilles75,
author = "Liskov, Barbara and Zilles, Steven",
title = "Specification Techniques for Data Abstractions",
journal = "IEEE Transactions on Software Engineering",
year = "1975",
volume = "SE-1",
pages = "7--19",
}
@InProceedings{ LitvinchoukPratt77,
author = "Litvinchouk, S. D. and Pratt, Vaughn R.",
title = "A Proof-Checker for Dynamic Logic",
booktitle = "Proceedings 5th Joint Conference on Artificial Intelligence",
year = "1977",
pages = "552--558",
}
@techreport{ LopesKiczales97:tr,
author = "Cristina Videira Lopes and Gregor Kiczales",
title = "{D}: {A} Language Framework for Distributed Programming",
institution = {Xerox PARC},
number = "SPL97-010",
month = "February",
address = "Palo Alto, CA, USA",
year = "1997",
url = "citeseer.nj.nec.com/lopes97language.html" }
@Article{ Loveman77,
author = "Loveman, D. B.",
title = "Program Improvement by Source-to-Source
Transformation",
journal = "Journal of the ACM",
year = "1977",
volume = "24",
pages = "121--145",
}
@Article{ LuckhamSuzuki77,
author = "Luckham, D. C. and Suzuki, N.",
title = "Proof of Termination within a Weak Logic of Programs",
journal = "Acta Informatica",
year = "1977",
volume = "8",
pages = "21--36",
}
@Book{ MacLane71,
author = "MacLane, Saunders",
title = "Categories for the Working Mathematician",
publisher = Springer,
year = "1971",
address = "Berlin, Heidelberg, New York",
}
@InProceedings{ MacQueen84,
author = "MacQueen, David B.",
title = "Modules for Standard {ML}",
booktitle = "{\lfp{1984}}",
year = "1984",
pages = "198--207",
}
@Article{ MacQueenPlotkinSethi,
author = "MacQueen, David B. and Plotkin, Gordon D. and Sethi, Ravi",
title = "An Ideal Model for Recursive Polymorphic Types",
journal = "Information and Control",
year = "1986",
volume = "71",
number = "1,2",
pages = "95-130",
}
@InProceedings{ Mairson90,
author = "Mairson, Harry",
title = "Deciding {ML} Typability is Complete for Deterministic Exponential
Time",
booktitle = "{\popl{17th}}",
year = "1990",
pages = "382--401",
}
@Article{ Majster77,
author = "Majster, M. E.",
title = "Limits of the Algebraic Specification of Data Types",
journal = "SIGPLAN Notices",
year = "1977",
volume = "12",
number = "10",
pages = "37--42",
month = "October",
}
@Article{ Malenfantetal96,
author = {Jacques Malenfant and Christophe Dony and Pierre Cointe},
title = {A Semantics of Introspection in a Reflective
Prototype-Based Language},
journal = {Lisp and Symbolic Computation},
year = 1996,
volume = 9,
number = {2/3},
month = {May/June},
pages = {153-180}
}
@Book{ Manna74,
author = "Manna, Zohar",
title = "Mathematical Theory of Computation",
publisher = "McGraw-Hill",
year = "1974",
address = "New York",
}
@Article{ MannaPnueli70,
author = "Manna, Zohar and Pnueli, Amir",
title = "Formalization of Properties of Functional Programs",
journal = "Journal of the ACM",
year = "1970",
volume = "17",
pages = "555--569",
}
@Article{ MannaShamir76,
author = "Manna, Zohar and Shamir, A.",
title = "The Theoretical Aspect of the Optimal Fixed Point",
journal = "SIAM Journal on Computing",
year = "1976",
volume = "5",
pages = "414--426",
}
@Article{ MannaVuillemin72,
author = "Manna, Zohar and Vuillemin, Jean",
title = "Fixpoint Approach to the Theory of Computation",
journal = "Communications of the ACM",
year = "1972",
volume = "15",
pages = "528--536",
}
@Article{ MannaWaldinger78,
author = "Manna, Zohar and Waldinger, Richard",
title = "Is `Sometime' Sometimes Better Than `Always'?",
journal = "Communications of the ACM",
year = "1978",
volume = "21",
pages = "159--172",
}
@Article{ MarcottyLedgardBochman76,
author = "Marcotty, F. and Ledgard, H. F. and Bochman, G. W.",
title = "A Sampler of Formal Definitions",
journal = "Computing Surveys",
year = "1976",
volume = "8",
pages = "191--276",
}
@Article{ Markowsky77,
author = "Markowsky, G.",
title = "Categories of Chain-Complete Posets",
journal = "Theoretical Computer Science",
year = "1977",
pages = "125--135",
}
@InProceedings{ Martin-Lof79,
author = "Martin-L{\"o}f, Per",
title = "Constructive Mathematics and Computer Programming",
booktitle = "Proceedings 6th International Congress for Logic,
Methodology, and Philosophy of Science",
year = "1979",
address = "Hannover",
month = aug,
}
@Article{ MasonTalcott91,
author = "Ian A. Mason and Carolyn L. Talcott",
title = "Equivalence in Functional Languages with Effects",
journal = "Journal of Functional Programming",
year = "1991",
volume = "1",
OPTnumber = "",
pages = "287-327",
OPTmonth = "",
OPTnote = ""
}
@InProceedings{ Masuhara-Kiczales-Dutchyn02:FOAL,
author = "Kidehiko Masuhara and Gregor Kiczales and Chris
Dutchyn",
title = "Compilation Semantics of Aspect-Oriented Programs",
pages = "17--26",
booktitle = "FOAL 2002 Proceedings: Foundations of Aspect-Oriented
Languages Workshop at AOSD 2002",
year = "2002",
editor = "Gary T. Leavens and Ron Cytron",
organization = "Department of Computer Science, Iowa State
University",
series = "Technical Report 02-06",
OPTnumber = "02-06",
month = apr,
url = "ftp://ftp.cs.iastate.edu/pub/techreports/TR02-06/TR.pdf",
}
@InProceedings{ MasuharaKiczales:ecoop03,
author = {Hidehiko Masuhara and Gregor Kiczales},
title = {Crosscutting in Aspect-Oriented Mechanisms},
booktitle = ecoop,
year = 2003,
publisher = {ACM Press},
address = {New York},
note = {To appear}
}
@Article{ McCarthy60,
author = "McCarthy, John",
title = "Recursive Functions of Symbolic Expressions
and their Computation by Machine, Part I",
journal = "Communications of the ACM",
year = "1960",
volume = "3",
pages = "184--195",
}
@InProceedings{ McCarthy62,
author = "McCarthy, John",
title = "Towards a Mathematical Science of Computation",
booktitle = "Information Processing 62",
year = "1962",
editor = "Popplewell",
pages = "21--28",
publisher = "North-Holland",
address = "Amsterdam",
}
@InCollection{ McCarthy63,
author = "McCarthy, John",
title = "A Basis for a Mathematical Theory of Computation",
booktitle = "Computer Program\-ming and Formal Systems",
publisher = "North-Holland",
year = "1963",
editor = "Braffort and Hirschberg",
pages = "33--70",
address = "Amsterdam",
}
@InProceedings{ McCarthy77,
author = "McCarthy, John",
title = "Epistemological Problems of Artificial
Intelligence",
booktitle = "Proceedings 5th International Joint Conference on Artificial Intelligence",
year = "1977",
pages = "1038--1044",
}
@InCollection{ McCarthy81,
author = "McCarthy, John",
title = "History of {LISP}",
booktitle = "History of Programming Languages",
publisher = "Academic Press",
year = "1981",
editor = "R. L. Wexelblatt",
pages = "173--197",
address = "New York",
}
@Book{ McCarthyEtAl65,
title = "LISP 1.5 Programmer's Manual",
author = "McCarthy, John and others",
publisher = "MIT Press",
address = "Cambridge, MA",
year = "1965",
}
@InCollection{ McCarthyPainter67,
author = "McCarthy, John and Painter, J.",
title = "Correctness of a Compiler for Arithmetic Expressions",
booktitle = "Proceedings Symposium in Applied Mathematics,
Vol. 19, Mathematical Aspects of Computer Science",
year = "1967",
editor = "J. T. Schwartz",
pages = "33--41",
publisher = "American Mathematical Society",
address = "Providence, RI",
}
@Unpublished{ McCarthyTalcott,
author = "McCarthy, John and Talcott, C.",
title = "{LISP}: Programming and Proving",
note = "in preparation",
}
@Article{ McDermott80,
author = "McDermott, D.",
title = "The Prolog Phenomenon",
journal = "SIGART Newsletter",
year = "1980",
number = "72",
pages = "16--20",
month = jul,
}
@InProceedings{ Meunieretal01,
author = {Philippe Meunier and Robby Findler and Paul
A. Steckler and Mitchell Wand},
title = {Selectors Make Analyzing Case-Lambda Too Hard},
booktitle = {Proc. Scheme 2001 Workshop},
OPTcrossref = {},
OPTkey = {},
OPTeditor = {Manuel Serrano},
OPTvolume = {},
OPTnumber = {},
series = {Technical Report: Informatique, Signaux et Systemes de Sophia-Antipolis, I3S/RT-2001-12-FR},
year = {2001},
OPTorganization = {},
OPTpublisher = {},
OPTaddress = {},
month = sep,
pages = "54-64",
URL = ftpdir # {meunier-etal-01.ps},
abstract = {Flanagan's set-based analysis (SBA) uses
selectors to choose data flowing through
expressions. For example, the rng selector chooses
the ranges of procedures flowing through an
expression. The MrSpidey static debugger for PLT
Scheme is based on Flanagan's formalism. In PLT
Scheme, a case-lambda is a procedure with possibly
several argument lists and clauses. When a
case-lambda is applied at a particular call site, at
most one clause is actually invoked, chosen by the
number of actual arguments. Therefore, an analysis
should propagate data only through appropriate
case-lambda clauses. MrSpidey propagates data
through all clauses of a case-lambda, lessening its
usefulness as a static debugger. Wishing to retain
Flanagan's framework, we extended it to better
analyze case-lambda with rest parameters by
annotating selectors with arity information. The
resulting analysis gives strictly better results
than MrSpidey. Unfortunately, the improved analysis
is too expensive because of overheads imposed by the
use of selectors. Nonetheless, a closure-analysis
style SBA (CA-SBA) eliminates these overheads and can
give comparable results within cubic time.},
source = {papers/scheme-01},
OPTannote = {}
}
@Article{ Meyer82,
author = "Meyer, Albert R.",
title = "What Is a Model of the Lambda Calculus?",
journal = "Information and Control",
year = "1982",
volume = "52",
pages = "87--122",
}
@InProceedings{ Meyer84,
author = {Albert R. Meyer},
title = {Thirteen Puzzles in Programming Logic},
booktitle = {Proceedings of the Workshop on Formal Software
Development: Combining Specification Methods},
OPTcrossref = {},
OPTkey = {},
editor = {D. Bj{\o}rner},
OPTvolume = {},
OPTnumber = {},
series = lncs,
year = {1984},
OPTorganization = {},
publisher = springer,
address = springeraddr,
month = may,
OPTpages = {},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@InProceedings{ MeyerSieber88,
author = "Meyer, Albert R. and Sieber, Kurt",
title = "Towards Fully Abstract Semantics for Local
Variables: Preliminary Report",
booktitle = "{\popl{15th}}",
year = "1988",
pages = "191--203",
}
@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 = "Berlin, Heidelberg, New York",
series = lncs,
volume = "193",}
@Proceedings{ Meyrowitz86,
title = "OOPSLA '86 Conference Proceedings",
year = "1986",
editor = "Meyrowitz, N.",
note = "{\it SIGPLAN Notices 21\/}(11) (November, 1986)",
}
@TechReport{ MichaylovPfenning91,
author = "Michaylov, Spiro and Pfenning, Frank",
title = "Natural Semantics and Some of its Meta-Theory in {Elf}",
institution = "Carnegie-Mellon University",
year = "1991",
type = "Technical Report",
number = "ERGO-91-101",
month = aug,
}
@Article{ Michie68,
author = {Donald Michie},
title = {`{M}emo' functions and machine learning},
journal = {Nature},
year = 1968,
volume = 218,
pages = {19-22}
}
@TechReport{ MilneMilner,
author = "Milne, George and Milner, Robin",
title = "Concurrent Processes and their Syntax",
institution = "University of Edinburgh, Department of Computer Science",
year = "1977",
type = "Internal Report",
number = "CSR-2-77",
month = may,
}
@Book{ MilneStrachey76,
author = "Milne, Robert and Strachey, Christopher",
title = "A Theory of Programming Language Semantics",
publisher = "Chapman and Hall",
year = "1976",
address = "London",
note = "Also Wiley, New York"
}
@TechReport{ Milner77,
author = "Milner, R.",
title = "Flowgraphs and Flow Algebras",
institution = "University of Edinburgh, Department of Computer Science",
year = "1977",
type = "Internal Report",
number = "CSR-5-77",
month = jul,
}
@Article{ Milner77a,
author = "Robin Milner",
title = "Fully abstract models of typed lambda-calculi",
journal = "Theoretical Computer Science",
year = "1977",
volume = "4",
OPTnumber = "",
pages = "1-22",
OPTmonth = "",
OPTnote = ""
}
@Article{ Milner78,
author = "Milner, R.",
title = "A Theory of Type Polymorphism in Programming",
journal = "Journal of Computer and Systems Science",
year = "1978",
volume = "17",
pages = "348--375",
}
@Article{ Milner92,
author = "Robin Milner",
title = "Functions as Processes",
journal = "Mathematical Structures in Computer Science",
year = 1992,
volume = "2",
OPTnumber = "2",
pages = "119--141",
OPTmonth = "",
OPTnote = ""
}
@InCollection{ MilnerEncycl,
author = "Robin Milner",
title = "Operational and Algebraic Semantics of Concurrent Processes",
booktitle = "Handbook of Theoretical Computer Science",
publisher = "MIT Press/Elsevier",
year = "1990",
editor = "Jan van Leeuwen",
OPTchapter = "",
pages = "1201-1242",
OPTaddress = "",
OPTmonth = "",
OPTnote = ""
}
@InProceedings{ MilnerMorrisNewey75,
author = "Milner, R. and Morris, Lockwood and Newey, Malcolm",
title = "A Logic for Computable Functions with Reflexive and Polymorphic Types",
booktitle = "Proceedings Conference on Proving and Improving Programs",
year = "1975",
address = "Arc-et-Senans",
}
@Article{ MilnerParrowWalker92,
author = "Robin Milner and Joachim Parrow and D. Walker",
title = "A calculus of mobile processes (parts I and II)",
journal = "Information and Computation",
year = 1992,
volume = "100",
pages = "1-77",
}
@Book{ MilnerTofteHarper89,
author = "Robin Milner and Mads Tofte and Robert Harper",
title = "The Definition of Standard ML",
publisher = "MIT Press",
year = "1989",
address = "Cambridge, MA",
}
@InCollection{ MilnerWeyrauch72,
author = "Milner, R. and Weyrauch, Richard",
title = "Proving Compiler Correctness in a Mechanized Logic",
booktitle = "Machine Intelligence 7",
publisher = "Edinburgh University Press",
year = "1972",
editor = "B. Meltzer and D. Michie",
pages = "51--72",
}
@Book{ Minsky67,
author = "Minsky, Marvin L.",
title = "Computation: Finite and Infinite Machines",
publisher = "Prentice-Hall",
year = "1967",
address = "Englewood Cliffs, NJ",
}
@Article{ Minsky70,
author = "Minsky, Marvin L.",
title = "Form and Content in Computer Science",
journal = "Journal of the ACM",
year = "1970",
volume = "17",
pages = "197--215",
}
@InCollection{ Minsky75,
author = "Minsky, Marvin L.",
title = "A Framework for Representing Knowledge",
booktitle = "The Psychology of Computer Vision",
publisher = "McGraw-Hill",
year = "1975",
editor = "Winston",
pages = "211--277",
address = "New York",
}
@InProceedings{ MishraReddy85,
author = "Mishra, Prateek and Reddy, Uday S.",
title = "Declaration-Free Type Checking",
booktitle = "{\popl{12th}}",
year = "1985",
pages = "7--21",
}
@InProceedings{ Mitchell84,
author = "Mitchell, John C.",
title = "Coercion and Type Inference (summary)",
booktitle = "{\popl{11th}}",
year = "1984",
pages = "175--185",
}
@InProceedings{ Mitchell86a,
author = "Mitchell, John C.",
title = "Representation Independence and Data Abstraction",
booktitle = "{\popl{13th}}",
year = "1986",
pages = "263--276",
}
@InProceedings{ Mitchell86b,
author = "Mitchell, John C.",
title = "A Type-Inference Approach to Reduction
Properties and Semantics of Polymorphic Expressions",
booktitle = "{\lfp{1986}}",
year = "1986",
pages = "308--319",
}
}
@Article{ Mitchell91,
author = "Mitchell, John C.",
title = "Type Inference with Simple Subtypes",
journal = "Journal of Functional Programming",
year = "1991",
volume = "1",
pages = "245--285",
}
@Book{ Mitchell96,
author = {John C. Mitchell},
ALTeditor = {},
title = {Foundations for Programming Languages},
publisher = {MIT Press},
year = {1996},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
address = {Cambridge, MA},
OPTedition = {},
OPTmonth = {},
OPTnote = {},
OPTannote = {}
}
@article{ MogensenJFP,
author = "Torben \AE. Mogensen",
title = "Efficient Self-Interpretation in Lambda Calculus",
journal = "Journal of Functional Programming",
volume = 2,
number = 3,
month = jul,
year = 1992,
pages = "345-364",
}
@InProceedings{ MogensenPepm,
author = "Torben \AE. Mogensen",
title = "Self-applicable Partial Evaluation for Pure Lambda Calculus",
year = "1992",
editor = "Charles Consel",
pages = "116--121",
booktitle = "ACM SIGPLAN Workshop on Partial Evaluation and
Semantics-Based Program Manipulation",
OPTmonth = jun,
OPTnote = "Yale University Department of Computer Science
Technical Report YALEU/DCS/RR-909"
}
@article{ Moggi:ic91,
author = "Eugenio Moggi",
title = "Notions of Computation and Monads",
journal = "Information and Computation",
volume = "93",
number = "1",
pages = "55-92",
year = "1991",
url = "citeseer.nj.nec.com/moggi89notions.html" }
@PhDThesis{ Montenyohl86,
author = "Montenyohl, Margaret",
title = "Static Analysis Based on Denotational Transformations",
school = "Indiana University",
year = "1986",
address = "Bloomington, IN",
}
@Article{ MontenyohlWand89,
author = "Montenyohl, Margaret and Wand, Mitchell",
title = "Incorporating Static Analysis in a Semantics-Based Compiler",
journal = "Information and Computation",
year = "1989",
volume = "82",
pages = "151--184",
}
@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"
}
@InProceedings{ Moon86,
author = "D. A. Moon",
editor = "Norman Meyrowitz",
title = "Object-Oriented Programming with {Flavors}",
pages = "1--8",
booktitle = oopsla,
Xbooktitle = "Proceedings of the Conference on Object-Oriented
Programming Systems, Languages, and Applications
(OOPSLA)",
OPTjournal = "SIGPLAN Notices",
OPTvolume = "21",
OPTnumber = "11",
month = nov,
year = "1986",
publisher = "ACM Press",
address = "New York, NY",
}
@Article{ Moore89,
author = "J. Strother Moore",
title = "A Mechanically Verified Language Implementation",
journal = "Journal of Automated Reasoning",
pages = "461--492",
volume = "5",
number = "4",
month = dec,
year = "1989",
}
@article{ Moreau:hosc98,
author = {Luc Moreau},
title = {A Syntactic Theory of Dynamic Binding},
journal = {Higher-Order and Symbolic Computation},
year = {1998},
pages = {233-279},
jpagecount = {47},
volume = 11,
number = 3,
month = dec,
issn = {1388-3690}
}
@PhDThesis{ Morris68,
author = "Morris, Jr., James H.",
title = "Lambda Calculus Models of Programming Languages",
school = "MIT",
year = "1968",
address = "Cambridge, MA",
}
@Article{ MorrisWegbreit77,
author = "Morris, Jr., James H. and Wegbreit, Ben",
title = "Subgoal Induction",
journal = "Communications of the ACM",
year = "1977",
volume = "20",
pages = "209--222",
}
@InProceedings{ Morrisett-popl98,
key = "Morrisett, {\em et al.}",
author = "Greg Morrisett and David Walker and Karl Crary and
Neal Glew",
title = "From System {F} to Typed Assembly Language",
booktitle = popl25,
year = "1998",
organization = "ACM",
address = "New York, NY",
month = jan,
pages = "85--97",
annote = "96 references.",
}
@Article{ Moses70,
author = "Moses, Joel",
title = "The Function of {FUNCTION} in {LISP}",
journal = "SIGSAM Bulletin",
year = "1970",
volume = "15",
pages = "13--27",
month = jul,
}
@InCollection{ Mosses74,
author = "Mosses, Peter D.",
title = "The Semantics of Semantic Equations",
booktitle = {\mfcs{1974}},
publisher = Springer,
year = "1974",
pages = "409--422",
address = "Berlin, Heidelberg, New York",
series = lncs,
volume = "28",}
@PhDThesis{ Mosses75,
author = "Mosses, Peter D.",
title = "Mathematical Semantics and Compiler Generation",
school = "Oxford University",
year = "1975",
type = "D. {Phil.} thesis",
}
@InCollection{ Mosses76,
author = "Mosses, Peter D.",
title = "Compiler Generation Using Denotational Semantics",
booktitle = "{\mfcs{1976}}",
publisher = springer,
year = "1976",
pages = "436--441",
address = "Berlin, Heidelberg, New York",
series = lncs,
volume = "45",
}
@Unpublished{ Mosses77,
author = "Mosses, Peter D.",
title = "Making Denotational Semantics Less Concrete",
note = "Extended Abstract of a Presentation at Workshop on
Semantics of Programming Languages, Bad Honnef, Germany, 21--25,
March 1977, to appear in a University of Dortmund Technical Report",
year = "1977",
}
@TechReport{ Mosses79,
author = "Mosses, Peter D.",
title = "SIS --- Semantics Implementation System: Reference Manual and User Guide",
institution = "Department of Computer Science University of Aarhus",
year = "1979",
number = "DAIMI MD-30",
address = "Denmark",
month = aug,
}
@InProceedings{ Mosses80,
author = "Mosses, Peter D.",
title = "A Constructive Approach to Compiler Correctness",
booktitle = "Automata, Languages, and Programming, Seventh Colloquium",
year = "1980",
}
@InProceedings{ Mosses81,
author = "Mosses, Peter D.",
title = "A Semantic Algebra for Binding Constructs",
booktitle = "Proceedings of International Colloquium on Formalization of Programming Concepts",
year = "1981",
address = "Peniscola, Spain",
month = apr,
}
@InProceedings{ Mosses82,
author = "Mosses, Peter D.",
title = "Abstract Semantic Algebras!",
booktitle = "Formal Descriptions of Programming Concepts II,
Proceedings IFIP TC-2 Working Conference,
Garmisch-Partenkirchen 1982",
year = "1983",
editor = "D. Bjorner",
pages = "63--88",
organization = "IFIP",
publisher = "North-Holland",
}
@Book{ Muchnick97,
author = {Steven S. Muchnick},
title = {Advanced Compiler Design and Implementation},
publisher = {Morgan Kaufmann Publishers},
year = 1997
}
@InProceedings{ MuchnickPleban80,
author = "Muchnick, Steven and Pleban, Uwe",
title = "A Semantic Comparison of {LISP} and {SCHEME}",
booktitle = "Conference Record of the 1980 LISP Conference",
year = "1980",
}
@Article{ Muller92,
author = "Robert Muller",
title = "{M-LISP}: {A} Representation-Independent Dialect of
{LISP} with Reduction Semantics",
journal = "ACM Transactions on Programming Languages and
Systems",
volume = "14",
number = "4",
pages = "589--616",
month = oct,
year = "1992",
coden = "ATPSDT",
ISSN = "0164-0925",
url = "http://www.acm.org/pubs/toc/Abstracts/0164-0925/133254.html",
abstract = "In this paper we introduce M-LISP, a dialect of LISP
designed with an eye toward reconciling LISP's
metalinguistic power with the {\em structural} style of
operational semantics advocated by Plotkin [28]. We
begin by reviewing the original definition of LISP [20]
in an attempt to clarify the source of its
metalinguistic power. We find that it arises from a
problematic clause in this definition. We then define
the abstract syntax and operational semantics of
M-LISP, essentially a hybrid of M-expression LISP and
Scheme. Next, we tie the operational semantics to the
corresponding equational logic. As usual, provable
equality in the logic implies operational equality.\par
Having established this framework we then extend M-LISP
with the metalinguistic {\em eval} and {\em reify}
operators (the latter is a nonstrict operator that
converts its argument to its metalanguage
representation). These operators encapsulate the
matalinguistic representation conversions that occur
globally in S-expression LISP. We show that the naive
versions of these operators render LISP's equational
logic inconsistent. On the positive side, we show that
a naturally restricted form of the {\em eval} operator
is confluent and therefore a conservative extension of
M-LISP. Unfortunately, we must weaken the logic
considerably to obtain a consistent theory of
reification.",
acknowledgement = ack-pb,
keywords = "languages; theory",
subject = "{\bf F.3.2}: Theory of Computation, LOGICS AND
MEANINGS OF PROGRAMS, Semantics of Programming
Languages, Operational semantics. {\bf D.3.2}:
Software, PROGRAMMING LANGUAGES, Language
Classifications, LISP. {\bf D.3.1}: Software,
PROGRAMMING LANGUAGES, Formal Definitions and Theory.
{\bf D.3.3}: Software, PROGRAMMING LANGUAGES, Language
Constructs and Features. {\bf D.3.4}: Software,
PROGRAMMING LANGUAGES, Processors. {\bf F.3.3}: Theory
of Computation, LOGICS AND MEANINGS OF PROGRAMS,
Studies of Program Constructs. {\bf F.4.1}: Theory of
Computation, MATHEMATICAL LOGIC AND FORMAL LANGUAGES,
Mathematical Logic, Lambda calculus and related
systems.",
}
@TechReport{ Musser77,
author = "Musser, David R.",
title = "A Proof Rule for Functions",
institution = "University of Southern California Information Sciences Institute",
year = "1977",
type = "Technical Report",
number = "ISI/RR-77-62",
address = "Marina del Rey, CA",
month = oct,
}
@InProceedings{ NadathurMiller88,
author = "Nadathur, G. and Miller, D.",
title = "An Overview of {$\lambda$-Prolog}",
booktitle = "Logic Programming: Proceedings of the 5th International Conference and Symposium",
year = "1988",
editor = "Kowalski and Bowen",
pages = "810--827",
publisher = "MIT Press",
address = "Cambridge, MA",
}
@TechReport{ NakajmaEtAl77,
author = "Nakajma, R. and Honda, M. and Nakahara, H.",
title = "Proving Abstract Specifications to be Valid for their Program
Implementations",
institution = "University of Oslo, Institute of Informatics",
year = "1977",
type = "Report",
number = "20",
month = sep,
note = "Appeared in {\it Acta Informatica} ?"
}
@PhDThesis{ Nicholson87,
author = "Nicholson, Tim",
title = "A Denotational Semantics and Machine Architecture for
Prolog",
school = "University of Sydney",
year = "1987",
}
@Article{ Nielson85,
author = {Flemming Nielson},
title = {Program Transformations in a Denotational Setting},
journal = {ACM Transactions on Programming Languages and Systems},
year = {1985},
OPTkey = {},
volume = {7},
number = {3},
month = jul,
pages = {359-379},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@InProceedings{ NielsonNielson86,
author = "Nielson, Hanne Riis and Nielson, Flemming",
title = "Semantics
Directed Compiling for Functional Languages",
booktitle = "{\lfp{1986}}",
year = "1986",
pages = "249--257",
}
@Article{ NielsonNielson88,
author = "Nielson, Flemming and Nielson, Hanne Riis",
title = "Two-Level Semantics and Code Generation",
journal = "Theoretical Computer Science",
year = "1988",
volume = "56",
pages = "59--133",
}
@InProceedings{ NielsonNielson93,
author = "Flemming Nielson and Hanne Riis Nielson",
title = "From CML to Process Algebras",
booktitle = "Proceesings of CONCUR '93",
year = 1993,
pages = "493-508",
publisher = springer,
address = springeraddr
}
@InProceedings{ NielsonNielson97,
author = {Flemming Nielson and Hanne Riis Nielson},
title = {Infinitary Control Flow Analysis: a Collecting Semantics
for Closure Analysis},
booktitle = popl24,
year = 1997,
organization = {ACM},
month = jan,
pages = {332-345}
}
@InProceedings{ NielsonNielson98,
author = "Hanne Riis Nielson and Flemming Nielson",
title = "Flow Logics for Contraint Based Analysis",
booktitle = "Compiler Construction CC'98",
year = "1998",
OPTeditor = "Kai Koskimies",
volume = "1383",
series = lncs,
pages = "109--127",
publisher = springer,
address = springeraddr,
abstract = "Flow logic offers a compact and versatile notation for
expressing the acceptability of solutions to program
analysis problems. In contrast to previous logical
formulations of program analysis it aims at integrating
existing approaches to data flow analysis and control
flow analysis. It is able to deal with a broad variety
of language paradigms, program properties, kinds of
formal semantics, and methods used for computing the
best solution. In this paper we illustrate how a
compositional flow logic (in ``succinct'' form) can be
systematically transformed into an efficient exhaustive
procedure for computing the best solution of a set of
constraints generated. This involves transformations to
attribute grammars and to specifications of the
(``verbose'') form used in control flow analysis.",
}
@InProceedings{ NielsonNielson99,
author = "F. Nielson and H. R. Nielson",
title = "Interprocedural Control Flow Analysis",
booktitle = "European Symposium on Programming 1999",
series = lncs,
publisher = springer,
address = springeraddr,
volume = "1576",
pages = "20--39",
year = "1999",
coden = "LNCSD9",
ISSN = "0302-9743",
bibdate = "Tue Sep 14 06:09:05 MDT 1999",
acknowledgement = ack-nhfb,
keywords = "ESOP; ETAPS; programming; software",
}
@Book{ Nilsson71,
author = "Nilsson, Nils J.",
title = "Problem-Solving Methods in Artificial Intelligence",
publisher = "McGraw-Hill",
year = "1971",
address = "New York",
}
@InProceedings{ Nipkow91,
author = "Tobias Nipkow",
title = "Higher-Order Critical Pairs",
booktitle = "{\lics{6th}}",
year = "1991",
pages = "342-349",
}
@InProceedings{ O'Donnell77a,
author = "O'Donnell, Michael",
title = "Subtree Replacement Systems: A Unifying
Theory for Recursive Equations, {LISP}, {Lucid}, and Combinatory Logic",
booktitle = "Proceedings 9th ACM Symposium on Theory of Computing",
year = "1977",
pages = "295--305",
address = "Boulder, CO",
}
@Book{ O'Donnell77b,
author = "O'Donnell, Michael",
title = "Computing in Systems Described by Equations",
publisher = springer,
year = "1977",
volume = "58",
series = lncs,
address = springeraddr,
}
@InProceedings{ O'TooleGifford89,
author = "O'Toole, James W. and Gifford, David K.",
title = "Type Reconstruction with First-Class Polymorphic Values",
booktitle = "Proceedings SIGPLAN '89 Conference on Programming Language Design and Implementation",
year = "1989",
note = "{\it SIGPLAN Notices}, 24(7):218--226, July 1989"
}
@inproceedings{ Odersky94,
author = {Odersky, Martin},
title = {A Functional Theory of Local Names},
booktitle = {Conference Record of POPL '94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
dates = {January 17--21},
year = {1994},
place = {Portland, Oregon},
pages = {48--59},
checked = {24 February 1995}
}
@Article{ OhearnTennent95,
author = "P. W. O'Hearn and R. D. Tennent",
title = "Parametricity and local variables",
journal = "Journal of the ACM",
month = "May",
year = "1995",
volume = "42(3)",
pages = "658--709",
}
@PhDThesis{ Oliva93,
author = "Dino P. Oliva",
title = "Advice on Structuring Compiler Back Ends and Proving
Them Correct",
school = "Northeastern University",
year = 1993,
month = dec,
}
@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",
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{ Oppen80,
author = "Oppen, Derek C.",
title = "Reasoning About Recursively Defined Data Structures",
journal = "Journal of the ACM",
year = "1980",
volume = "27",
number = "3",
pages = "403--411",
month = jul,
}
@InProceedings{ OssherTarr:ICSE2000,
author = {Harold Ossher and Peri Tarr},
title = {{Hyper/J}: multi-dimensional separation of concerns
for {Java}},
booktitle = {Proceedings of the 22nd International Conference on
Software Engineering, June 4-11, 2000, Limerick, Ireland},
OPTcrossref = {},
OPTkey = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
year = {2000},
OPTorganization = {ACM},
publisher = {ACM},
address = {New York},
OPTmonth = {},
pages = {734-737},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@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{ Pagan76,
author = "Pagan, Frank G.",
title = "On Interpreter-Oriented Definitions of Programming Languages",
journal = "Computer Journal",
year = "1976",
volume = "19",
number = "2",
pages = "151--155",
}
@Article{ Palsberg95,
author = "Jens Palsberg",
title = "Closure Analysis in Constraint Form",
journal = "ACM Transactions on Programming Languages and
Systems",
volume = "17",
number = "1",
pages = "47--62",
month = jan,
year = "1995",
coden = "ATPSDT",
ISSN = "0164-0925",
bibdate = "Fri Jan 5 07:58:42 MST 1996",
url = "http://www.acm.org/pubs/toc/Abstracts/0164-0925/201001.html",
abstract = "Flow analyses of untyped higher-order functional
programs have in the past decade been presented by
Ayers, Bondorf, Consel, Jones, Heintze, Sestoft,
Shivers, Steckler, Wand, and others. The analyses are
usually defined as abstract interpretations and are
used for rather different tasks such as type recovery,
globalization, and binding-time analysis. The analyses
all contain a global {\em closure analysis\/} that
computes information about higher-order control-flow.
Sestoft proved in 1989 and 1991 that closure analysis
is correct with respect to call-by-name and
call-by-value semantics, but it remained open if
correctness holds for arbitrary beta-reduction.\par
This article answers the question; both closure
analysis and others are correct with respect to
arbitrary beta-reduction. We also prove a
subject-reduction result: closure information is still
valid after beta-reduction. The core of our proof
technique is to define closure analysis using a
constraint system. The constraint system is equivalent
to the closure analysis of Bondorf, which in turn is
based on Sestoft's.",
acknowledgement = ack-nhfb,
keywords = "languages; theory",
subject = "{\bf D.3.1}: Software, PROGRAMMING LANGUAGES, Formal
Definitions and Theory, Semantics. {\bf D.3.2}:
Software, PROGRAMMING LANGUAGES, Language
Classifications, Applicative languages. {\bf F.3.1}:
Theory of Computation, LOGICS AND MEANINGS OF PROGRAMS,
Specifying and Verifying and Reasoning about Programs,
Logics of programs. {\bf F.4.3}: Theory of Computation,
MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Formal
Languages, Operations on languages. {\bf F.3.2}: Theory
of Computation, LOGICS AND MEANINGS OF PROGRAMS,
Semantics of Programming Languages, Operational
semantics. {\bf D.3.4}: Software, PROGRAMMING
LANGUAGES, Processors, Optimization.",
}
@InProceedings{ PalsbergOKeefe95,
author = {Jens Palsberg and Patrick M. O'Keefe},
title = {A Type System Equivalent to Flow Analysis},
booktitle = popl22,
year = 1995,
organization = {ACM},
month = jan,
pages = {367-378}
}
@Book{ PalsbergSchwartzbach94,
author = {Jens Palsberg and Michael I. Schwartzbach},
title = {Object-Oriented Type Systems},
publisher = {Wiley Professional Computing},
year = 1994,
address = {Chichester}
}
@Article{ PalsbergSchwartzbach95,
author = "Jens Palsberg and Michael I. Schwartzbach",
title = "Safety Analysis versus Type Inference",
journal = "Information and Computation",
volume = 118,
number = 1,
pages = "128--141",
year = 1995}
@Unpublished{ PalsbergWand00,
author = {Jens Palsberg and Mitchell Wand},
title = {{CPS} Transformation of Flow Information},
note = {to appear in {\em Journal of Functional Programming}},
year = {2003},
URL = ftpdir # {palsberg-wand-00.ps},
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/cps-flow-99}
}
@Article{ PalsbergWand:jfp03,
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. },
}
@Book{ Pareigis70,
author = "Pareigis, B.",
title = "Categories and Functors",
publisher = "Academic Press",
year = "1970",
}
@InProceedings{ Parikh78,
author = "Parikh, Rohit",
title = "A Decidability Result for a Second Order Process
Logic",
booktitle = "Proceedings 19th Annual Symposium on Foundations of Computer Science",
year = "1978",
pages = "177--183",
publisher = "IEEE",
}
@Inproceedings{ Park81,
author="David Park",
title="Concurrency and Automata on Infinite Sequences",
booktitle="Theoretical Computer Science: 5th GI-Conference, Karlsruhe",
editor="Peter Deussen",
year=1981,
month=mar,
publisher=springer,
address = springeraddr,
series=lncs,
volume=104,
pages= {167-183}
}
@Article{ Parnas72,
author = "Parnas, David L.",
title = "A Technique for Module Specification with Examples",
journal = "Communications of the ACM",
year = "1972",
volume = "15",
number = "5",
pages = "330--336",
month = may,
}
@Article{ PartschPepper76,
author = "Partsch, H. and Pepper, P.",
title = "A Family of Rules for Recursion Removal",
journal = "Information Processing Letters",
year = "1976",
volume = "5",
pages = "174--177",
}
@InProceedings{ Paulson82,
author = "Paulson, Lawrence C.",
title = "A Semantics-Directed Compiler Generator",
booktitle = "{\popl{9th}}",
year = "1982",
pages = "224--233",
}
@Article{ Paulson89,
author = "Paulson, Lawrence C.",
title = "The Foundation of a Generic Theorem Prover",
journal = "Journal of Automated Reasoning",
year = "1989",
volume = "5",
pages = "363--397",
}
@Book{ Paulson91,
author = "Paulson, Lawrence C.",
title = "ML for the Working Programmer",
publisher = "Cambridge University Press",
year = "1991",
}
@Book{ PeytonJones87,
author = "Peyton Jones, Simon L.",
title = "The Implementation of Functional Programming Languages",
publisher = "Prentice-Hall International",
year = "1987",
}
@InProceedings{ PeytonJonesWadler93,
author = "Peyton Jones, Simon L. and Philip L. Wadler",
title = "Imperative Functional Programming",
booktitle = popl20,
year = 1993,
pages = "71-84",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
OPTnote = ""
}
@inproceedings{ Pfenning91,
key = "Pfenning91" ,
author = "Frank Pfenning" ,
title = "Logic Programming in the {LF} Logical Framework" ,
booktitle= "Logical Frameworks" ,
editor = "G. Huet and G. Plotkin" ,
publisher= "Cambridge University Press" ,
pages = "149--181",
year = "1991"
}
@InProceedings{ PfenningElliott88,
author = "Pfenning, Frank and Elliott, Conal",
title = "Higher-Order Abstract Syntax",
booktitle = "Proceedings SIGPLAN '88 Conference on Programming
Language Design and Implementation",
year = "1988",
pages = "199--208",
month = jun,
}
@Unpublished{ PfenningLee89,
author = "Pfenning Frank and Lee, Peter",
title = "Reflection in the polymorphic lambda-calculus",
note = "manuscript",
year = "1989",
}
@Unpublished{ Pierce93,
author = "Benjamin Pierce",
title = "Concurrent OO Language Design",
note = "presentation at Workshop on Foundations of
Object-Oriented Languages (Palo Alto)",
year = 1993,
month = oct,
}
@incollection{ Pitts95,
author = {A. M. Pitts},
title = {Operationally-Based Theories of Program Equivalence},
booktitle = {Semantics and Logics of Computation},
editor = {P. Dybjer and A. M. Pitts},
publisher = {Cambridge University Press},
year = {1995},
note = {Based on lectures given at the CLICS-II Summer School on
Semantics and Logics of Computation, Isaac Newton Institute for
Mathematical Sciences, Cambridge UK, September 1995.},
citation-source = {Greg Sullivan, Thu Jun 27 11:28:21 1996}
}
@InProceedings{ PittsStark93,
author = {Andrew M. Pitts and Ian D. B. Stark},
title = {Observable properties of higher order functions that
create local names, or: What's new?},
booktitle = {Mathematical Foundations of Computer Science,
Proc. 18th Intl. Symp, Gdansk, 1993},
volume = 711,
series = lncs,
year = 1993,
publisher = springer,
address = springeraddr,
pages = {122-141},
abstract= {The research reported in this paper is concerned with the
problem of reasoning about properties of higher order functions
involving state. It is motivated by the desire to identify what, if
any, are the difficulties created purely by {\em locality\/} of
state, independent of other properties such as side-effects,
exceptional termination and non-termination due to recursion. We
consider a simple language (equivalent to a fragment of Standard ML)
of typed, higher order functions that can dynamically create fresh
{\em names\/}; names are created with local scope, can be tested for
equality and can be passed around via function application, but that
is all. Despite the extreme simplicity of the language and its
operational semantics, the observable properties of such functions
are shown to be very subtle. A notion of `logical relation' is
introduced which incorporates a version of {\em representation
independence\/} for local names. We show how to use it to establish
observational equivalences. The method is shown to be complete (and
decidable) for expressions of first order types, but incomplete at
higher types.}
}
@InCollection{ PittsStark98,
author = {Andrew Pitts and Ian Stark},
title = {Operational Reasoning for Functions with Local
State},
booktitle = {Higher Order Operational Techniques in Semantics},
editor = {Andrew Gordon and Andrew Pitts},
year = {1998},
pages = {227--273},
publisher = {Publications of the Newton Institute, Cambridge
University Press},
url = {http://www.ed.ac.uk/~stark/operfl.html},
}
@Article{ Plotkin75,
author = "Plotkin, Gordon D.",
title = "Call-by-Name, Call-by-Value and the {$\lambda$}-Calculus",
journal = "Theoretical Computer Science",
year = "1975",
volume = "1",
pages = "125--159",
}
@Article{ Plotkin76,
author = "Plotkin, Gordon D.",
title = "A Powerdomain Construction",
journal = "SIAM Journal on Computing",
year = "1976",
}
@Article{ Plotkin77,
author = "Plotkin, Gordon D.",
title = "{LCF} Considered as a Programming Language",
journal = "Theoretical Computer Science",
year = "1977",
volume = "5",
pages = "223--255",
}
@TechReport{ Plotkin81,
author = "Plotkin, Gordon D.",
title = "A Structural Approach to Operational Semantics",
institution = "Aarhus University",
year = "1981",
number = "DAIMI FN-19",
OPTaddress = "",
OPTmonth = Sept,
OPTnote = ""
}
@InProceedings{ PlotkinMitchell84,
author = "Plotkin, Gordon D. and Mitchell, John C.",
title = "Abstract Types have Existential Type",
booktitle = "{\popl{12th}}",
year = "1985",
note = "Revised version to appear in {\it ACM Transactions On Programming Languages and Systems}",
}
@InProceedings{ PlotkinPower01,
author = "Gordon Plotkin and John Power",
title = "Adequacy for Algebraic Effects",
booktitle = "Foundations of Software Science and Computation Structures (FOSSACS)",
series = lncs,
address = springeraddr,
volume = "2030",
OPTpages = "1--??",
year = "2001",
coden = "LNCSD9",
ISSN = "0302-9743",
bibdate = "Sat Feb 2 13:03:47 MST 2002",
url = "http://link.springer-ny.com/link/service/series/0558/bibs/2030/20300001.htm;
http://link.springer-ny.com/link/service/series/0558/papers/2030/20300001.pdf",
acknowledgement = ack-nhfb,
}
@inproceedings{ PlotkinPower:fossacs02,
author = "Gordon D. Plotkin and John Power",
title = "Notions of Computation Determine Monads",
booktitle = "Foundations of Software Science and Computation Structures (FOSSACS)",
pages = "342--356",
year = "2002",
series = lncs,
address = springeraddr,
volume = "2620",
url = "citeseer.nj.nec.com/plotkin02notions.html" }
@InProceedings{ PlotkinSmyth77,
author = "Plotkin, Gordon D. and Smyth, Michael B.",
title = "The Category-Theoretic Solution of Recursive Domain Equations",
booktitle = "Proceedings 18th IEEE Symposium on Foundations of Computer Science",
year = "1977",
address = "Providence, RI",
}
@Article{ Pottinger81,
author = "Pottinger, Garrel",
title = "The Church-Rosser Theorem for the Typed {$\lambda$}-Calculus with Surjective Pairing",
journal = "Notre Dame Journal of Formal Logic",
year = "1981",
volume = "22",
pages = "264--268",
}
@Book{ Prather76,
author = "Prather, R.",
title = "Discrete Mathematical Structures for Computer Science",
publisher = "Houghton-Mifflin",
year = "1976",
address = "Boston",
}
#Unpublished{ Reistad92,
author = {Brian Reistad},
title = {Macros That Work in {M}odula-2},
year = {1992},
month = oct,
note = {Unpublished paper},
}
@Book{ Pratt75,
author = "Pratt, Terrence W.",
title = "Programming Languages: Design and Implementation",
publisher = "Prentice-Hall",
year = "1975",
address = "Englewood Cliffs, NJ",
}
@InProceedings{ Pratt76,
author = "Pratt, Vaughn R.",
title = "Semantical Considerations on {Floyd-Hoare} Logic",
booktitle = "Proceedings 17th IEEE Symposium on Foundations of Computer Science",
year = "1976",
pages = "109--121",
}
@InProceedings{ Pratt78a,
author = "Pratt, Vaughn R.",
title = "A Practical Decision Method for Propositional Dynamic Logic",
booktitle = "Proceedings 10th ACM Symposium on Theory of Computing",
year = "1978",
pages = "326--337",
}
@TechReport{ Pratt78b,
author = "Pratt, Vaughn R.",
title = "Six Lectures on Dynamic Logic",
institution = "Massachusetts Institute of Technology, Laboratory for Computer Science",
year = "1978",
number = "MIT/LCS/TM-117",
address = "Cambridge, MA",
month = dec,
}
@Book{ PreparataYeh73,
author = "Preparata, Franco P. and Yeh, Raymond T.",
title = "Introduction to Discrete Structures",
publisher = "Addison-Wesley",
year = "1973",
address = "Reading, MA",
}
@Book{ Quine60,
author = "Quine, W. V. O.",
title = "Word and Object",
publisher = "MIT Press",
year = "1960",
address = "Cambridge, MA",
}
@Book{ Ralston65,
author = "Ralston, Anthony",
title = "A First Course in Numerical Analysis",
publisher = "McGraw-Hill",
year = "1965",
address = "New York",
}
@Book{ RandellRussell64,
author = "B. Randell and L. J. Russell",
title = "{Algol} 60 implementation",
publisher = "Academic Press",
address = "New York, NY",
year = "1964",
}
@Article{ RaoultSethi83,
author = "Raoult, Jean-Claude and Sethi, Ravi",
title = "Properties of a notation for combining functions",
journal = "Journal of the ACM",
year = "1983",
volume = "30",
pages = "595-611",
}
@InProceedings{ RaoultSethi84,
author = "Raoult, Jean-Claude and Sethi, Ravi",
title = "The Global Storage Needs of a Subcomputation",
booktitle = " {\popl{11th}}",
year = "1984",
pages = "148--157",
}
@InCollection{ RaskovskyCollier80,
author = "Raskovsky, M. and Collier, P.",
title = "From Standard to Implementation Denotational
Semantics",
booktitle = "Semantics-Directed Compiler Generation",
publisher = springer,
year = "1980",
editor = "Neil D. Jones",
address = springeraddr,
series = lncs,
volume = "94",
}
@misc{ Rauglaudre03camlp4manual,
author = "Daniel de Rauglaudre",
title = "Camlp4 Reference Manual",
url = "http://caml.inria.fr/pub/docs/manual-camlp4/index.html",
year = {2003},
note = "{\hfill\\ }http://caml.inria.fr/pub/docs/manual-camlp4/index.html",
}
@Book{ Reade89,
author = "Reade, C.",
title = "Elements of Functional Programming",
publisher = "Addison-Wesley",
year = "1989",
address = "Reading, MA",
}
@TechReport{ RebohSacerdoti73,
author = "Reboh, R. and Sacerdoti, E. D.",
title = "A Preliminary {QLISP} Manual",
institution = "SRI Artificial Intelligence Center",
year = "1973",
type = "Technical Note",
number = "81",
month = aug,
}
@InProceedings{ Reddy88,
author = "Reddy, Uday S.",
title = "Objects as Closures: Abstract Semantics of Object
Oriented Languages",
booktitle = "{\lfp{1988}}",
year = "1988",
pages = "289--297",
}
@Article{ ReesClingerEtAl86,
author = "Rees, Jonathan A. and Clinger, William D. and others",
key = "RC86",
title = "Revised{$^3$} Report on the Algorithmic Language {Scheme}",
journal = "SIGPLAN Notices",
year = "1986",
volume = "21",
number = "12",
pages = "37--79",
month = dec,
}
@Article{ Reiss90,
author = "Steven P. Reiss",
title = "Connecting tools using message passing in the {Field}
environment",
journal = "IEEE Software",
volume = "7",
number = "4",
pages = "57--66",
month = jul,
year = "1990",
coden = "IESOEG",
ISSN = "0740-7459",
bibdate = "Sat Jan 25 07:35:26 MST 1997",
abstract = "Field connects tools with selective broadcasting,
which follows the Unix philosophy of letting
independent tools cooperate through simple conventions.
Field demonstrates that this simple approach is
feasible and desirable.",
acknowledgement = ack-nhfb,
affiliation = "Brown Univ, Providence, RI, USA",
classification = "722; 723",
journalabr = "IEEE Software",
keywords = "Brown Workstation Environment; Computer Operating
Systems; Computer Software --- Software Engineering;
Design; Message Passing; Software Development
Environments",
}
@MastersThesis{ Reistad92,
author = {Brian Reistad},
title = {Macros That Work in {M}odula-2},
school = {University of Oregon},
year = {1992},
OPTkey = {},
OPTtype = {},
OPTaddress = {},
month = oct,
OPTnote = {},
OPTannote = {}
}
@Unpublished{ Remy88,
author = "R{\'e}my, Didier",
title = "Typechecking records and variants in a natural
extension of {ML}",
note = "manuscript",
year = "1988",
month = "May 9",
}
@InProceedings{ Remy89,
author = "R{\'e}my, Didier",
title = "Typechecking records and variants in a natural
extension of {ML}",
booktitle = "{\popl{16th}}",
year = "1989",
pages = "77--88",
}
@InProceedings{ Reppy91,
author = "J. H. Reppy",
booktitle = "{ACM} {SIGPLAN} '91 Conference on Programming Language
Design and Implementation, {SIGPLAN} Notices 26(6)",
pages = "294--305",
title = "{CML}: {A} Higher-order Concurrent Language",
year = "1991",
}
@InProceedings{ RepsTeitelbaum84,
author = "Reps, Thomas and Teitelbaum, Tim",
title = "The Synthesizer Generator",
booktitle = "Proceedings\ ACM SIGSOFT/SIGPLAN Software
Engineering\ Symposium\ on Practical Software Development Environments",
year = "1984",
note = "{\it SIGPLAN Notices},19(5) and {\it
Software Engineering Notes},9(3):42--48, May 1984"
}
@inproceedings{ ReusStreicher:icalp05,
author = {Bernhard Reus and
Thomas Streicher},
title = {About {H}oare Logics for Higher-Order Store.},
booktitle = {ICALP},
year = {2005},
pages = {1337-1348},
ee = {http://dx.doi.org/10.1007/11523468_108},
crossref = {icalp05},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@Article{ Reynolds70,
author = "Reynolds, John C.",
title = "GEDANKEN --- A Simple Typeless Language Based
on the Principle of Completeness and the Reference Concept",
journal = "Communications of the ACM",
year = "1970",
volume = "13",
pages = "308--319",
}
@InProceedings{ Reynolds72,
author = "Reynolds, John C.",
title = "Definitional Interpreters for Higher-Order Programming Languages",
booktitle = "Proceedings ACM National Conference",
year = "1972",
pages = "717--740",
}
@InCollection{ Reynolds74a,
author = "Reynolds, John C.",
title = "Towards a Theory of Type Structures",
booktitle = "Programming Symposium (Colloque sur la Programmation, Paris)",
series = lncs,
volume = "19",
publisher = springer,
year = "1974",
pages = "408--425",
address = springeraddr,
}
@InCollection{ Reynolds74b,
author = "Reynolds, John C.",
title = "On the Relation between Direct and Continuation Semantics",
booktitle = "Proceedings 2nd Colloquium on Automata, Languages, and
Programming, Saarbrucken, 1974",
series = lncs,
volume = "14",
publisher = springer,
year = "1974",
pages = "141--156",
address = springeraddr,
}
@InProceedings{ Reynolds75,
author = "Reynolds, John C.",
title = "User-Defined Types and Procedural Data
Structures as Complementary Approaches to Data Abstraction",
booktitle = "Conference on New Directions on Algorithmic Languages",
year = "1975",
organization = "IFIP WP 2.1",
address = "Munich",
month = aug,
}
@Article{ Reynolds77,
author = "Reynolds, John C.",
title = "Semantics of the Domain of Flow Diagrams",
journal = "Journal of the ACM",
year = "1977",
volume = "24",
pages = "484--503",
}
@InProceedings{ Reynolds78,
author = "Reynolds, John C.",
title = "Syntactic Control of Interference",
booktitle = "{\popl{5th}}",
year = "1978",
pages = "39--46",
}
@InCollection{ Reynolds81a,
author = "Reynolds, John C.",
title = "The Essence of {Algol}",
booktitle = "Algorithmic Languages",
publisher = "North-Holland",
year = "1981",
editor = "J. W. deBakker and J. C. van Vliet",
pages = "345--372",
address = "Amsterdam",
}
@Book{ Reynolds81b,
author = "Reynolds, John C.",
title = "The Craft of Programming",
publisher = "Prentice-Hall International",
year = "1981",
}
@InProceedings{ Reynolds83,
author = "Reynolds, John C.",
title = "Types, Abstractions, and Parametric Polymorphism",
booktitle = "Proceedings IFIP 83",
year = "1983",
}
@InCollection{ Reynolds85,
author = "Reynolds, John C.",
title = "Three Approaches to Type Structure",
booktitle = "Proceedings TAPSOFT Advanced Seminar on the Role of
Semantics in Software Development",
publisher = springer,
year = "1985",
series = lncs,
address = springeraddr,
month = mar,
}
@inproceedings{ Reynolds:lics02,
author = {John C. Reynolds},
title = {Separation Logic: A Logic for Shared Mutable Data Structures},
booktitle = lics02,
year = {2002},
isbn = {0-7695-1483-9},
pages = {55--74},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
}
@Article{ Rice65,
author = "Rice, H. G.",
title = "Recursion and Iteration",
journal = "Communications of the ACM",
year = "1965",
volume = "8",
pages = "114--115",
}
@inproceedings{ RitterPitts95,
author={E. Ritter and A. M. Pitts},
title={A Fully Abstract Translation between a $\lambda$-Calculus with
Reference Types and {Standard} {M}{L}},
booktitle={2nd Int. Conf. on Typed Lambda Calculus and Applications,
Edinburgh, 1995},
series={Lecture Notes in Computer Science},
volume={902},
publisher= springer,
address = springeraddr,
year=1995,
pages={397--413},
abstract={This paper describes a syntactic translation for a
substantial fragment of the core Standard ML language into a typed
lambda calculus with recursive types and imperative features in the
form of reference types. The translation compiles SML's use of
declarations and pattern matching into lambda terms, and transforms
the use of environments in the operational semantics into a simpler
relation of evaluation to canonical form. The translation is shown to
be `fully abstract', in the sense that it both preserves and reflects
observational equivalence (also commonly called contextual
equivalence). A co-inductively defined notion of applicative
bisimilarity for lambda calculi with state is developed to establish
this result.}
}
@Article{ Robinson65,
author = "Robinson, J. Alan",
title = "A Machine-Oriented Logic Based on the Resolution Principle",
journal = "Journal of the ACM",
year = "1965",
volume = "12",
pages = "23--41",
}
@InProceedings{ RobinsonEtAl75,
author = "Robinson, Lawrence and Levitt, Karl N. and Neumann, P. G. and
Saxena, A. R.",
title = "On Attaining Reliable Software for a Secure Operating System",
booktitle = "Proceedings - 1975 International Conference on Reliable Software",
year = "1975",
note = "{\it SIGPLAN Notices} 10:267--284",
month = apr,
}
@Article{ RobinsonLevitt77,
author = "Robinson, Lawrence and Levitt, Karl N.",
title = "Proof Techniques for Hierarchically Structured Programs",
journal = "Communications of the ACM",
year = "1977",
volume = "20",
number = "4",
pages = "271--283",
month = apr,
}
@TechReport{ RobinsonRoubine77,
author = "Robinson, Lawrence and Roubine, Oliver",
title = "SPECIAL --- A Specification and Assertion Language",
institution = "Stanford Research Institute",
year = "1977",
type = "Technical Report",
number = "CSL-46",
address = "Menlo Park, CA",
month = jan,
}
@InCollection{ RobinsonSibert81,
author = "Robinson, J. Alan and Sibert, Ernest E.",
title = "{LOGLISP}: an Alternative to {PROLOG}",
booktitle = "Machine Intelligence 10",
publisher = "Ellis Horwood Limited",
year = "1981",
editor = "J. E. Hayes and D. Michie and Y-H Pao",
pages = "399-419",
address = "Chichester",
note = "Also John Wiley, New York"
}
@Article{ Rosen73,
author = "Rosen, Barry K.",
title = "Tree Manipulating Systems and Church-Rosser Theorems",
journal = "Journal of the ACM",
year = "1973",
volume = "20",
pages = "160--187",
}
@Article{ Rosen80,
author = "Rosen, B. K.",
title = "How Practical is {POPL}?",
journal = "SIGPLAN Notices",
year = "1980",
volume = "15",
number = "1",
pages = "115--116",
month = jan,
}
@Misc{ Ruiz:CCM,
OPTkey = {},
author = {Diego Sevilla Ruiz},
title = {The {CORBA} \&\ {CORBA} {C}omponent Model ({CCM}) Page},
howpublished = {web page},
OPTyear = {},
OPTmonth = {},
note = {http://ditec.um.es/\char'176dsevilla/ccm/},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@Article{ Russell77,
author = "Russell, B.",
title = "On an Equivalence between Continuation and Stock Semantics",
journal = "Acta Infor\-ma\-tica",
year = "1977",
volume = "8",
pages = "113--124",
}
@InCollection{ Salwicki78,
author = "Salwicki, A.",
title = "On Algorithmic Theory of Stacks",
booktitle = {\mfcs{1978}},
publisher = springer,
year = "1978",
editor = "J. Winkowski",
series = lncs,
volume = "64",
pages = "452--461",
address = springeraddr,
}
@TechReport{ Sandewall70,
author = "Sandewall, Eric",
title = "A Proposed Solution to the {FUNARG} Problem",
institution = "Uppsala University, Department of Computer Sciences",
year = "1970",
type = "Report",
number = "29",
month = nov,
}
@Article{ Sandewall78,
author = "Sandewall, Eric",
title = "Programming in the Interactive Environment: The {LISP} Experience",
journal = "Computing Surveys",
year = "1978",
volume = "10",
number = "1",
pages = "35--72",
month = mar,
}
@article{ Sands:toplas96,
author = "David Sands",
title = "Total Correctness by Local Improvement in the Transformation of Functional Programs",
journal = "ACM Transactions on Programming Languages and Systems",
volume = "18",
number = "2",
month = "March",
publisher = "ACM Press",
pages = "175--234",
year = "1996",
url = "citeseer.ist.psu.edu/sands96total.html" }
@PhDThesis{ Sangiorgi92,
author = "Davide Sangiorgi",
title = "Expressing Mobility in Process Algebras: First-Order
and Higher-Order Paradigms",
school = "{Department of Computer Science, University of Edinburgh}",
year = 1992,
type = {{CST}--99--93},
note ={Also published as {ECS}--{LFCS}--93--266},
}
@Article{ Sangiorgi94,
author = {Davide Sangiorgi},
title = {The Lazy Lambda Calculus in a Concurrency Scenario},
journal = ic,
year = 1994,
volume = 111,
number = 1,
month = may,
pages = {120-153},
note = "Preliminary version appeared in {\lics{7th}}, 1992"
}
@article{ Sangiorgi:mscs98,
author = {Davide Sangiorgi},
title = {On the bisimulation proof method},
journal = {Mathematical Structures in Comp. Sci.},
volume = {8},
number = {5},
year = {1998},
issn = {0960-1295},
pages = {447--479},
doi = {http://dx.doi.org/10.1017/S0960129598002527},
publisher = {Cambridge University Press},
address = {New York, NY, USA},
}
@phdthesis{ Sastry94,
author = "Sastry, A.V.S. ",
title = "Efficient Array Update Analysis of Strict Functional Languages",
school = "Computer and Information Science, University of Oregon",
year = 1994}
@inproceedings{ SastryClinger94,
author = "Sastry, A.V.S. and Clinger, William ",
title = "Parallel destructive updating in strict functional languages",
booktitle = "ACM Conference on Lisp and Functional Programming",
pages = "263-272",
year = 1994,
series = "Lisp Pointers 7(3)",
}
@inproceedings{ SastryClingerAriola93,
author = "Sastry, A.V.S. and Clinger, William and Ariola, Zena ",
title = "Order-of-evaluation analysis for destructive updates in
strict functional languages with flat aggregates",
booktitle = "Conference on Functional Programming Languages
and Computer Architecture",
pages = "266-275",
year = 1993}
@Article{ Schmidt85,
author = "Schmidt, David A.",
title = "Detecting Global Variables in Denotational
Semantics",
journal = "ACM Transactions on Programming Languages and Systems",
year = "1985",
volume = "7",
pages = "299--310",
}
@Book{ Schmidt86,
author = "Schmidt, David A.",
title = "Denotational Semantics: A Methodology for
Language Development",
publisher = "Allyn and Bacon",
year = "1986",
address = "Boston",
}
@Unpublished{ Scott72a,
author = "Scott, Dana S.",
title = "Data Types as Lattices",
note = "Unpublished notes",
year = "1972",
address = "Amsterdam"
}
@InCollection{ Scott72b,
author = "Scott, Dana S.",
title = "Continuous Lattices",
booktitle = "Toposes, Algebraic Geometry, and Logic",
publisher = springer,
series = lncs,
volume = "274",
year = "1972",
editor = "F. William Lawvere",
pages = "97--136",
address = springeraddr,
}
@Article{ Scott76,
author = "Scott, Dana S.",
title = "Data Types as Lattices",
journal = "SIAM Journal on Computing",
year = "1976",
volume = "5",
pages = "522--587",
}
@Article{ Scott77,
author = "Scott, Dana S.",
title = "Logic and Programming Languages",
journal = "Communications of the ACM",
year = "1977",
volume = "20",
pages = "634--641",
}
@InCollection{ Scott80,
author = "Scott, Dana S.",
title = "Relating theories of the {$\lambda$}-calculus",
booktitle = "To H.B. Curry: Essays on Combinatory Logic,
Lambda-Calculus and Formalism",
publisher = "Academic Press",
year = "1980",
editor = "Hindley and Seldin",
pages = "403--450",
address = "New York and London",
}
@InProceedings{ Scott82,
author = "Scott, Dana S.",
title = "Domains for Denotational Semantics",
booktitle = "Proceedings International Colloquium on Automata, Languages, and Programming '82",
year = "1982",
}
@InCollection{ ScottStrachey72,
author = "Scott, Dana S. and Strachey, Christopher",
title = "Toward a Mathematical Semantics for Computer Languages",
booktitle = "Computers and Automata",
publisher = "Wiley",
year = "1972",
editor = "J. Fox",
pages = "19--46",
address = "New York",
}
@Article{ Sedgewick77,
author = "Sedgewick, R.",
title = "Permutation Generation Methods",
journal = "Computing Surveys",
year = "1977",
volume = "9",
number = "2",
pages = "137--164",
month = jun,
}
@MastersThesis{ Sestoft88,
author = "Peter Sestoft",
title = "Replacing Function Parameters by Global Variables",
school = "DIKU, University of Copenhagen",
year = 1988,
month = oct
}
@MastersThesis{ Sestoft89,
author = "Sestoft, Peter",
title = "Replacing function parameters by global variables",
school = "DIKU, University of Copenhagen",
year = "1989",
address = "Copenhagen"
}
@PhDThesis{ Sestoft91,
author = "Sestoft, Peter",
title = "Analysis and efficient implementation of functional programs",
school = "DIKU, University of Copenhagen",
year = "1991",
address = "Copenhagen"
}
@Article{ Sestoft97,
title = "Deriving a lazy abstract machine",
author = "Peter Sestoft",
pages = "231--264",
journal = "Journal of Functional Programming",
month = may,
year = "1997",
volume = "7",
number = "3",
references = "\cite{TCS::Josephs1989} \cite{POPL::Launchbury1993}
\cite{JFP::Jones1992} \cite{POPL::SansomJ1995}
\cite{POPL::Wand1982}",
}
@InProceedings{ Sethi81,
author = "Sethi, Ravi",
title = "Circular Expressions: elimination of static environments",
booktitle = "Automata, Languages, and Programming, 8{th} Colloquium,
Acre",
series = lncs,
volume = "115",
year = "1981",
publisher = springer,
address = springeraddr,
}
@Article{ Sethi83,
author = "Sethi, Ravi",
title = "Control Flow Aspects of Semantics-Directed Compiling",
journal = "ACM Transactions on Programming Languages and Systems",
year = "1983",
volume = "5",
pages = "554--596",
}
@Book{ Sethi89,
author = "Sethi, Ravi",
title = "Programming Languages: Concepts and Constructs",
publisher = "Addison-Wesley",
year = "1989",
address = "Reading, MA",
}
@Unpublished{ SethiTang78,
author = "Sethi, Ravi and Tang, Adrian",
title = "Transforming direct into
continuation semantics for a Simple Imperative Language",
note = "Unpublished manuscript",
OPTyear = "1978",
OPTmonth = apr,
}
@Article{ SethiTang80,
author = "Sethi, Ravi and Tang, Adrian",
title = "Constructing Call-by-value Continuation Semantics",
journal = "Journal of the ACM",
year = "1980",
volume = "27",
pages = "580--597",
}
@Article{ SethiUllman70,
author = "Sethi, Ravi and Ullman, Jeffrey D.",
title = "The Generation of Optimal Code for Arithmetic Expressions",
journal = "Journal of the ACM",
year = "1970",
volume = "17",
pages = "715--728",
}
@book{ Shalit96dylan,
author = "Andrew Shalit",
title = {The {D}ylan reference manual: the definitive guide to the new object-oriented dynamic language},
publisher = "Addison-Wesley",
year = {1996},
isbn = {0-201-44211-6},
url = "http://www.gwydiondylan.org/books/drm/",
}
@InProceedings{ Shao-pldi95,
author = "Zhong Shao and Andrew W. Appel",
title = "{A} Type-based Compiler for Standard {ML}",
booktitle = pldi95,
year = "1995",
address = "La Jolla, CA",
url = "ftp://daffy.cs.yale.edu/pub/papers/shao/tcps.ps",
month = jun,
pages = "116--129",
}
@inproceedings{ ShaoAppel94,
author = "Zhong Shao and Andrew W. Appel",
title = "Space-Efficient Closure Representations",
booktitle = lfp94,
pages = "150-161",
year = "1994",
url = "citeseer.nj.nec.com/183857.html",
note = {revised version appeared as "Efficient and safe-for-space closure
conversion", \emph{TOPLAS 22}, 2000, 129-161.}
}
@Book{ Shaw74,
author = "Shaw, Alan C.",
title = "The Logical Design of Operating Systems",
publisher = "Prentice-Hall",
year = "1974",
address = "Englewood Cliffs, NJ",
}
@Book{ ShawGarlan96,
author = "M. Shaw and D. Garlan",
title = "Software Architecture: Perspective on an Emerging
Discipline",
booktitle = "Software Architecture: Perspective on an Emerging
Discipline",
publisher = "Prentice-Hall",
publaddr = "Englewood Cliffs , NJ , USA",
year = "1996",
referencedby = "\cite{1996:tr:oreizy}, \cite{1997:icse:carzaniga}",
annote = "incomplete",
}
@inproceedings{ SheardPeytonJones:Haskell-02,
author = "Tim Sheard and Simon {Peyton Jones}",
title = "Template metaprogramming for {Haskell}",
booktitle = "ACM SIGPLAN Haskell Workshop 02",
year = 2002,
month = oct,
pages = "1-16",
editor = "Manuel M. T. Chakravarty",
publisher = "ACM Press"
}
@PhDThesis{ Shivers91,
author = "Olin Shivers",
title = "Control-Flow Analysis of Higher-Order Languages",
school = "Carnegie-Mellon University",
year = "1991",
OPTaddress = "",
month = may,
OPTnote = ""
}
@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},
OPTannote = {}
}
@Book{ Shoenfield67,
author = "Shoenfield, J. R.",
title = "Mathematical Logic",
publisher = "Addison-Wesley",
year = "1967",
address = "Reading, MA",
}
@InProceedings{ Shostak77,
author = "Shostak, Robert E.",
title = "An Algorithm for Reasoning About Equality",
booktitle = "Proceedings 5th International Joint Conference on
Artificial Intelligence",
year = "1977",
pages = "526--527",
}
@inproceedings{ Sieber:mfcs94,
author = {Kurt Sieber},
title = {Full abstraction for the second order subset of an ALGOL-like language},
booktitle = {MFCS '94: Selected papers from the 19th international symposium on Mathematical foundations of computer science},
year = {1996},
pages = {155--212},
location = {Kos\ˇice, Slovakia},
doi = {http://dx.doi.org/10.1016/S0304-3975(96)00066-7},
publisher = {Elsevier Science Publishers Ltd.},
address = {Essex, UK},
}
@article{ Sieber:tcs96,
author = {Kurt Sieber},
title = {Full abstraction for the second order subset of an ALGOL-like language},
journal = {Theor. Comput. Sci.},
volume = {168},
number = {1},
year = {1996},
issn = {0304-3975},
pages = {155--212},
doi = {http://dx.doi.org/10.1016/S0304-3975(96)00066-7},
publisher = {Elsevier Science Publishers Ltd.},
address = {Essex, UK},
}
@misc{ Skalsi04metaprogramming,
author = {Kamil Skalsi and Michal Moskal and Pawel Olszta},
title = "Meta-programming in {N}emerle",
note = "{\hfill\\ }http://nemerle.org/metaprogramming.pdf",
year = {2004},
}
@TechReport{ Smith82,
author = "Smith, Brian C.",
title = "Reflection and Semantics in a Procedural Language",
institution = "Massachusetts Institute of Technology",
year = "1982",
number = "MIT/LCS/TR-272",
address = "Cambridge, MA",
month = jan,
}
@InProceedings{ Smith84,
author = "Smith, Brian C.",
title = "Reflection and Semantics in {Lisp}",
booktitle = "{\popl{11th}}",
publisher = {ACM},
address = {New York},
year = "1984",
pages = "23--35",
}
@Article{ Smyth78,
author = "Smyth, Michael B.",
title = "Power Domains",
journal = "Journal of Computer and Systems Science",
year = "1978",
volume = "16",
pages = "23--36",
}
@Article{ SpitzenLevittRobinson78,
author = "Spitzen, Jay M. and Levitt, Karl N. and Robinson, Lawrence",
title = "An Example of Hierarchical Design and Proof",
journal = "Communications of the ACM",
year = "1978",
volume = "21",
pages = "1064--1075",
}
@misc{ SpiveySeres99,
author = "J. Spivey and S. Seres",
title = "Embedding Prolog in Haskell",
text = "J. M. Spivey and S. Seres, `Embedding Prolog in Haskell', in Proceedings
of Haskell'99 (E. Meier, ed.), Technical Report UUCS1999-28, Department
of Computer Science, University of Utrecht.",
year = "1999",
url = "citeseer.nj.nec.com/article/seres99embedding.html"
}
@Book{ SpringerFriedman89,
author = "Springer, George and Friedman, Daniel P.",
title = "Scheme and the Art of Programming",
publisher = "MIT Press",
year = "1989",
address = "Cambridge MA",
note = "Also New York, McGraw-Hill "
}
@Book{ StanatMcAllister77,
author = "Stanat, D. F. and McAllister, D. F.",
title = "Discrete Mathematics in Computer Science",
publisher = "Prentice-Hall",
year = "1977",
address = "Englewood Cliffs, NJ",
}
@InProceedings{ Stansifer88,
author = "Stansifer, Ryan",
title = "Type Inference with Subtypes",
booktitle = "{\popl{15th}}",
year = "1988",
pages = "88--97",
}
@PhdThesis{ Stark94,
author = "Ian Stark",
title = "Names and Higher-Order Functions",
school = "University of Cambridge",
year = 1994,
month = dec,
note = "Also published as Technical Report~363, University of
Cambridge Computer Laboratory"
}
@Article{ Statman82,
author = "Statman, Richard",
title = "Logical Relations and the Typed Lambda Calculus",
journal = "Information and Control",
year = "1985",
volume = "65",
pages = "85--97",
}
@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",
}
@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},
}
@TechReport{ Steele76,
author = "Steele, Guy L.",
title = "LAMBDA: The Ultimate Declarative",
institution = "Massachusetts Institute of Technology",
year = "1976",
type = "Artificial Intelligence Memo",
number = "379",
address = "Cambridge, MA",
month = oct,
}
@TechReport{ Steele77,
author = "Steele, Guy L.",
title = "Data Representations in PDP-10 MacLISP",
institution = "Massachusetts Institute of Technology",
year = "1977",
type = "Artificial Intelligence Memo",
number = "420",
address = "Cambridge, MA",
month = sep,
}
@TechReport{ Steele78,
author = "Steele, Guy L.",
title = "Rabbit: A Compiler for {Scheme}",
institution = "Massachusetts Institute of Technology",
year = "1978",
type = "Technical Report",
number = "474",
address = "Cambridge, MA",
month = may,
}
@Book{ Steele90,
author = "Steele, Guy L.",
title = "Common Lisp: the Language",
publisher = "Digital Press",
year = "1990",
address = "Burlington MA",
edition = "Second",
}
@inproceedings{ Steele:oopsla98,
author = {Guy L. Steele},
title = {Growing a language},
booktitle = {OOPSLA '98 Addendum: Addendum to the 1998 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum)},
year = {1998},
isbn = {1-58113-286-7},
location = {Vancouver, British Columbia, Canada},
doi = {http://doi.acm.org/10.1145/346852.346922},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@TechReport{ SteeleSussman76,
author = "Steele, Jr., Guy L. and Sussman, Gerald Jay",
title = "LAMBDA: The Ultimate Imperative",
institution = "Massachusetts Institute of Technology",
year = "1976",
type = "Artificial Intelligence Memo",
number = "353",
address = "Cambridge, MA",
month = mar,
}
@TechReport{ SteeleSussman78a,
author = "Steele, Guy L. and Sussman, Gerald Jay",
title = "The Revised Report on {SCHEME}",
institution = "Massachusetts Institute of Technology",
year = "1978",
type = "Artificial Intelligence Memo",
number = "452",
address = "Cambridge, MA",
month = jan,
}
@TechReport{ SteeleSussman78b,
author = "Steele, Guy L. and Sussman, Gerald Jay",
title = "The Art of the Interpreter or, the Modularity Complex (Parts Zero, One and Two)",
institution = "Massachusetts Institute of Technology",
year = "1978",
type = "Artificial Intelligence Memo",
number = "453",
address = "Cambridge, MA",
month = may,
}
@InProceedings{ SteeleSussman79,
author = "Steele, Guy L. and Sussman, Gerald Jay",
title = "The Dream of a Lifetime: A Lazy Scoping Mechanism",
booktitle = "Conference Record of the 1980 LISP Conference",
year = "1980",
pages = "163--172",
}
@Article{ SteeleSussman80,
author = "Steele, Guy L. and Sussman, Gerald Jay",
title = "Design of a {LISP}-Based Microprocessor",
journal = "Communications of the ACM",
year = "1980",
volume = "23",
pages = "628--645",
}
@Book{ Stoy77,
author = "Stoy, Joseph E.",
title = "Denotational Semantics: The Scott-Strachey
Approach to Programming Language Theory",
publisher = "MIT Press",
year = "1977",
address = "Cambridge, MA",
}
@Article{ Stoy81,
author = "Stoy, Joseph E.",
title = "The Congruence of Two Programming Language Definitions",
journal = "Theoretical Computer Science",
year = "1981",
volume = "13",
pages = "151--174",
}
@article{Strachey00,
author = {Christopher Strachey},
title = {Fundamental Concepts in Programming Languages},
journal = {Higher Order Symbol. Comput.},
volume = {13},
number = {1-2},
year = {2000},
issn = {1388-3690},
pages = {11--49},
publisher = {Kluwer Academic Publishers},
address = {Hingham, MA, USA},
}
@Unpublished{Strachey67,
author = {Christopher Strachey},
title = {Fundamental Concepts in Programming Languages},
note = {unpublished notes from International Summer School
on Programming Languages, Copenhagen},
year = 1967
}
@TechReport{ Strachey73,
author = "Strachey, Christopher",
title = "The Varieties of Programming Language",
institution = "Oxford University Computing Laboratory",
year = "1973",
type = "Technical Monograph",
number = "PRG-10",
}
@TechReport{ StracheyWadsworth74,
author = "Strachey, Christopher and Wadsworth, C. P.",
title = "Continuations: A Mathematical Semantics for Handling Full Jumps",
institution = "Oxford University Computing Laboratory",
year = "1974",
type = "Technical Monograph",
number = "PRG-11",
month = jan,
}
@Article{ StreicherReus98,
title = "Classical logic, continutation semantics and abstract
machines",
author = "Th. Streicher and B. Reus",
pages = "543--572",
journal = "Journal of Functional Programming",
month = nov,
year = "1998",
volume = "8",
number = "6",
references = "\cite{JFP::AbadiCCL1991} \cite{TCS::Curien1991}
\cite{TCS::FelleisenH1992} \cite{TCS::FelleisenFKD1987}
\cite{POPL::Griffin1990}",
}
@Article{ Strong71,
author = "Strong, H. R.",
title = "Translating Recursion Equations into Flow Charts",
journal = "Journal of Computer and Systems Science",
year = "1971",
volume = "5",
pages = "254--285",
}
@InProceedings{ Sudholt01,
author = {Remi Douence and Olivier Motelet and Mario Sudholt},
title = {A formal definition of crosscuts},
booktitle = {Proceedings of the Third International Conference
on Metalevel Architectures and Separation of
Crosscutting Concerns (Reflection 2001)},
volume = 2192,
series = lncs,
year = 2001,
publisher = springer,
address = springeraddr,
month = sep,
pages = {170-186}
}
@PhdThesis{ Sullivan97,
author = {Gregory T. Sullivan},
title = {Operationally-Based Models of Higher-Order Imperative
Programming Languages},
school = {Northeastern University},
year = 1997,
address = {Boston, MA},
month = aug
}
@inproceedings{ SumiiPierce:popl04,
author = {Eijiro Sumii and Benjamin C. Pierce},
title = {A bisimulation for dynamic sealing},
booktitle = {\popl{31st}},
year = {2004},
isbn = {1-58113-729-X},
pages = {161--172},
location = {Venice, Italy},
doi = {http://doi.acm.org/10.1145/964001.964015},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@inproceedings{ SumiiPierce:popl05,
author = {Eijiro Sumii and Benjamin C. Pierce},
title = {A bisimulation for type abstraction and recursion},
booktitle = {\popl{32nd}},
oldbooktitle = {POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
year = {2005},
isbn = {1-58113-830-X},
pages = {63--74},
location = {Long Beach, California, USA},
doi = {http://doi.acm.org/10.1145/1040305.1040311},
publisher = {ACM Press},
address = {New York, NY, USA},
}
@TechReport{ SussmanSteele75,
author = "Sussman, Gerald J. and Steele, Jr., Guy L.",
title = "SCHEME: An Interpreter for Extended Lambda Calculus",
institution = "Massachusetts Institute of Technology",
year = "1975",
type = "Artificial Intelligence Memo",
number = "349",
address = "Cambridge, MA",
month = dec,
}
@PhDThesis{ Suzuki76,
author = "Suzuki, N.",
title = "Automatic Verification of Programs with Complex Data Structures",
school = "Stanford University",
year = "1976",
type = "dissertation"
}
@InProceedings{ SweeneyTip98,
author = {Peter F. Sweeney and Frank Tip},
title = {A Study of Dead Data Members in {C}++ Applications},
booktitle = pldi98,
year = 1998,
organization = {ACM},
month = jun,
pages = {324-332}
}
@inproceedings{ TahaSheard:PEPM-97,
author = "W. Taha and T. Sheard",
title = "Multi-Stage Programming with Explicit Annotations",
booktitle = "Partial Evaluation and Seman\-tics-Based Program Manipulation, Amsterdam, The Netherlands, June 1997",
publisher = "New York:\ ACM",
pages = "203--217",
year = "1997",
url = "citeseer.ist.psu.edu/article/taha97multistage.html" }
@article{ Talcott00,
author = {di Blasio, P. and Fisher, K. and Talcott, C.},
title = {A Control-Flow Analysis for a Calculus of Concurrent Objects},
year = {2000},
volume = 26,
pages = {617-634},
journal = {IEEE Transactions on Software Engineering},
clt-url = {http://www-formal.stanford.edu/MT/00cfacco-tse.ps.gz},
abstract = {
We present a set-based control flow analysis for an imperative,
concurrent object calculus extending the Fisher-Honsell-Mitchell functional
object-oriented calculus. The analysis is shown to be sound with respect
to a transition system semantics.},
keywords = {concurrent object-oriented, control-flow analysis, soundness,
prototype-based},
}
@Article{ Talcott93,
author = "Carolyn Talcott",
title = "A Theory of Binding Structures and Applications to
Rewriting",
journal = "Theoretical Computer Science",
volume = 112,
year = 1993,
pages = "99-143",
}
@Book{ Tanenbaum76,
author = "Tanenbaum, A. S.",
title = "Structured Computer Organization",
publisher = "Prentice-Hall",
year = "1976",
address = "Englewood Cliffs, NJ",
}
@InProceedings{ Tarditi-pldi96,
author = "D. Tarditi and G. Morrisett and P. Cheng and C. Stone
and R. Harper and P. Lee",
title = "{TIL}: {A} Type-Directed Optimizing Compiler for
{ML}",
booktitle = pldi96,
year = "1996",
pages = "181--192",
url = "http://www.acm.org/pubs/articles/proceedings/pldi/231379/p181-tarditi/p181-tarditi.pdf",
genterms = "MEASUREMENT, PERFORMANCE, VERIFICATION",
categories = "D.3.4 Software, PROGRAMMING LANGUAGES, Processors.
D.3.3 Software, PROGRAMMING LANGUAGES, Language
Constructs and Features.",
annote = "incomplete",
}
@Book{ Tarski46,
author = "Tarski, A.",
title = "Introduction to Logic and to the Methodology
of Deductive Sciences",
publisher = "Oxford University Press",
year = "1946",
address = "New York",
edition = "Second",
}
@PhDThesis{ Tennent73,
author = "Tennent, Robert D.",
title = "Mathematical Semantics and Design of Programming Languages",
school = "Department of Computer Science, University of Toronto",
year = "1973",
}
@Article{ Tennent76,
author = "Tennent, Robert D.",
title = "Denotational Semantics of Programming Languages",
journal = "Communicatios of the ACM",
year = "1976",
volume = "19",
pages = "437--453",
}
@Article{ Thatcher70,
author = "Thatcher, James W.",
title = "Generalized Sequential Machines",
journal = "Journal of Computer and Systems Science",
year = "1970",
volume = "4",
pages = "339--367",
}
@InProceedings{ ThatcherWagnerWright78,
author = "Thatcher, James W. and Wagner, Eric G. and Wright, Jesse B.",
title = "Data Type Specifications: Parameteriza\-tion and the Power of
Specification Techniques",
booktitle = "Proceedings 10th Annual ACM Symposium on Theory of Computing",
year = "1978",
pages = "119--132",
address = "San Diego",
}
Need to fix booktitle
@InCollection{ ThatcherWagnerWright79,
author = "Thatcher, James W. and Wagner, Eric G. and Wright, Jesse B.",
title = "More on Advice on Structuring Compilers and Proving Them Correct",
booktitle = "Automata, Languages, and Programming, Sixth Colloqui\-um, Graz, July 1979",
publisher = springer,
year = "1979",
editor = "H. A. Maurer",
pages = "596--615",
series = lncs,
volume = "71",
address = springeraddr,
}
@Article{ ThatcherWagnerWright81,
author = "Thatcher, James W. and Wagner, Eric G. and Wright, Jesse B.",
title = "More on Advice on Structuring Compilers and Proving Them Correct",
journal = "Theoretical Computer Science",
year = "1981",
volume = "15",
pages = "223--250",
}
@InProceedings{ Thatte88,
author = "Thatte, Satish",
title = "Type Inference with Partial Types",
booktitle = "Proceedings International Colloquium on Automata,
Languages, and Programming '88",
year = "1988",
pages = "615--629",
}
@Article{ Thatte94,
author = "Thatte, Satish",
title = "Type Inference with Partial Types",
journal = "Theoretical Computer Science",
year = "1994",
volume = "124",
OPTnumber = "",
pages = "127-148",
OPTmonth = "",
OPTnote = "preliminary version appeared in ICALP '88"
}
@InProceedings{ Thomsen89,
author = "Bent Thomsen",
title = "A Calculus of Higher Order Communicating Systems",
booktitle = "\popl{16th}",
year = 1989,
pages = "143--154",
}
@article{ TipPalsberg00,
author = "Frank Tip and Jens Palsberg",
title = "Scalable propagation-based call graph construction algorithms",
journal = "ACM SIG{\-}PLAN Notices",
volume = "35",
number = "10",
pages = "281--293",
year = "2000",
url = "citeseer.nj.nec.com/tip00scalable.html" }
@Unpublished{ TiurynWand95b,
author = "Jerzy Tiuryn and Mitchell Wand",
title = "Adding Input-Output to PCF (Technical Summary)",
note = "submitted for publication",
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."
}
@PhDThesis{ Tofte87,
author = "Tofte, Mads",
title = "Operational Semantics and Polymorphic Type Inference",
school = "University of Edinburgh",
year = "1987",
type = "{PhD} dissertation",
}
@InProceedings{ TofteTalpin94,
author = {Mads Tofte and Jean-Pierre Talpin},
title = {Implementation of the typed call-by-value $\lambda$-calculus
using a stack of regions},
booktitle = popl21,
year = 1994,
pages = {188-201}
}
@InCollection{ TrakhtenbrotHalpernMeyer83,
author = "Trakhtenbrot, Boris A. and Halpern, Joseph Y. and Meyer, Albert R.",
title = "From Denotational to Operational and Axiomatic Semantics:
An Overview",
booktitle = "Logics of Programs",
publisher = springer,
year = "1983",
series = lncs,
}
@Book{ TremblayManohar75,
author = "Tremblay, J. T. and Manohar, R. P.",
title = "Discrete Mathematical Structures with Applications to Computer Science",
publisher = "McGraw-Hill",
year = "1975",
address = "New York",
}
@Book{ Troelstra73,
title = "Metamathematical Investigation of Intuitionistic Arithmetic and Analysis",
publisher = springer,
year = "1973",
editor = "Troelstra, A. S.",
volume = "344",
series = "Lecture Notes in Mathematics",
address = springeraddr,
}
@InProceedings{ TuckerKrishnamurthi:aosd03,
author = {David B. Tucker and Shriram Krishnamurthi},
title = {Pointcuts and Advice in Higher-Order Languages},
booktitle = aosd,
OPTcrossref = {},
OPTkey = {},
editor = {Mehmet Ak\c{s}it},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
year = {2003},
OPTorganization = {},
publisher = {ACM Press},
address = {New York},
month = mar,
pages = {158-167},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@InProceedings{ Turchin80,
author = "Turchin, Valentin F.",
title = "The Use of Metasystem Transition in Theorem
Proving and Program Optimization",
booktitle = "Automata, Languages, and Programming, Seventh Colloquium",
year = "1980",
}
@article{Turing36,
author = {Turing, A. M.},
title = {{On Computable Numbers, with an Application to the
Entscheidungsproblem}},
journal = {Proc. London Math. Soc.},
volume = {42},
series = {2nd},
number = {1},
pages = {230-265},
doi = {10.1112/plms/s2-42.1.230},
year = {1936},
URL = {http://plms.oxfordjournals.org},
eprint =
{http://plms.oxfordjournals.org/cgi/reprint/s2-42/1/230.pdf}
}
@Article{ Turing37,
author = "Turing, A. M.",
title = "The $p$ -functions in {$\lambda$}-{$K$}-conversion",
journal = "Journal of Symbolic Logic",
year = "1937",
volume = "2",
pages = "164",
}
@Article{ Turner79,
author = "Turner, David A.",
title = "A New Implementation Technique for Applicative Languages",
journal = "Software-Practice and Experience",
year = "1979",
volume = "9",
pages = "31--49",
}
@Article{ Vuillemin74,
author = "Vuillemin, Jean",
title = "Correct and Optimal Implementations of
Recursion in a Simple Program\-ming Language",
journal = "Journal of Computer and Systems Science",
year = "1974",
volume = "9",
pages = "332--354",
}
@InProceedings{ Wadler85,
author = "P. L. Wadler",
title = "How to replace failure by a list of successes",
editor = "Jean-Pierre Jouannaud",
booktitle = "Functional Programming Languages and Computer
Architecture",
publisher = "Springer Verlag",
series = "Lecture Notes in Computer Science",
volume = "201",
month = sep,
year = "1985",
pages = "113--128",
reffrom = "Frost:Launchbury:bcs:cj:1989",
reffrom = "Wadler:acm:lfp:1990",
}
@inproceedings{ Wadler92,
author = "Philip Wadler",
title = "The Essence of Functional Programming",
booktitle = "Conference Record of the Nineteenth Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages",
address = "Albequerque, New Mexico",
publisher = "ACM",
pages = "1--14",
year = "1992",
url = "citeseer.nj.nec.com/wadler92essence.html" }
@Article{ Wadsworth76,
author = "Wadsworth, C. P.",
title = "The relation between computational and
denotational properties for {Scott}'s {$D_\infty$}-models of the lambda-calculus",
journal = "SIAM Journal on Computing",
year = "1976",
volume = "5",
pages = "488-521",
}
@InCollection{ Wadsworth80,
author = "Christopher P. Wadsworth",
title = "Some Unusual $\lambda$-calculus Numeral Systems",
booktitle = "To H.B. Curry: Essays on Combinatory Logic,
Lambda-Calculus and Formalism",
publisher = "Academic Press",
year = "1980",
editor = " J. R. Seldin and J. P. Hindley",
pages = "215-230",
address = "New York and London",
}
@inproceedings{ Wagner71,
author = {Wagner, Eric G.},
title = {An algebraic theory of recursive definitions and recursive languages},
booktitle = {STOC '71: Proceedings of the third annual ACM symposium on Theory of computing},
year = {1971},
pages = {12--23},
location = {Shaker Heights, Ohio, United States},
doi = {http://doi.acm.org/10.1145/800157.805034},
publisher = {ACM},
address = {New York, NY, USA},
}
@InProceedings{ Walker91,
author = "David Walker",
title = "{$\pi$}-Calculus Semantics of Object-Oriented
Programming Languages",
booktitle = "Proc.\ Conference on Theoretical Aspects of Computer
Software",
year = 1991,
series = lncs,
publisher = springer,
address = springeraddr,
}
@InProceedings{ WalkerZdancewicLigatti:icfp03,
author = {David Walker and Steve Zdancewic and Jay Ligatti},
title = {A Theory of Aspects},
booktitle = icfp,
OPTcrossref = {},
OPTkey = {},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
year = {2003},
OPTorganization = {},
publisher = {ACM},
address = {Uppsala, Sweden},
OPTmonth = {},
OPTpages = {},
OPTnote = {This proceedings},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@Unpublished{ Wand02,
author = {Mitchell Wand},
title = {Analyses that Distinguish Different Evaluation Orders, or,
Unsoundness Results in Control-Flow Analysis},
note = {unpublished note},
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 = {}
}
@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",
}
@Article{ Wand75,
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",
}
@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",
}
@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,
}
@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",
}
@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",
}
@Article{ Wand79b,
author = "Wand, Mitchell",
title = "Fixed-Point Constructions in Order-Enriched Categories",
journal = "Theoretical Computer Science",
year = "1979",
volume = "8",
pages = "13--30",
}
@Article{ Wand80a,
author = "Wand, Mitchell",
title = "Continuation-Based Program Transformation Strategies",
journal = "Journal of the ACM",
year = "1980",
volume = "27",
pages = "164--180",
}
@TechReport{ Wand80b,
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,
}
@Article{ Wand80c,
author = "Wand, Mitchell",
title = "First-Order Identities as a Defining Language",
journal = "Acta Informatica",
year = "1980",
volume = "14",
pages = "337--357",
}
@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,
}
@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",
}
@Article{ Wand82a,
author = "Wand, Mitchell",
title = "Specifications, Models, and Implementations of Data
Abstractions",
journal = "Theoretical Computer Science",
year = "1982",
volume = "20",
pages = "3-32",
}
@InProceedings{ Wand82b,
author = "Wand, Mitchell",
title = "Semantics-Directed Machine Architecture",
booktitle = "{\popl{9th}}",
year = "1982",
pages = "234--241",
}
@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,
}
@InProceedings{ Wand83a,
author = "Wand, Mitchell",
title = "Loops in Combinator-Based Compilers",
booktitle = "{\popl{10th}}",
year = "1983",
pages = "190--196",
}
@Article{ Wand83b,
author = "Wand, Mitchell",
title = "Loops in Combinator-Based Compilers",
journal = "Information ~and Control",
year = "1983",
volume = "57",
number = "2--3",
pages = "148--164",
month = "May/June",
}
@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,
}
@Article{ Wand84a,
author = "Wand, Mitchell",
title = "What is {Lisp}?",
journal = "American Mathematical Monthly",
year = "1984",
volume = "91",
pages = "32--42",
}
@InProceedings{ Wand84b,
author = "Wand, Mitchell",
title = "A Types-as-Sets Semantics for {Milner}-style Polymorphism",
booktitle = "{\popl{11th}}",
year = "1984",
pages = "158--164",
}
@InProceedings{ Wand84c,
author = "Wand, Mitchell",
title = "A Semantic Prototyping System",
booktitle = "Proceedings ACM SIGPLAN '84 Compiler Construction Conference",
year = "1984",
pages = "213--221",
}
@InProceedings{ Wand85a,
author = "Wand, Mitchell",
title = "Embedding Type Structure in Semantics",
booktitle = "{\popl{12th}}",
year = "1985",
pages = "1--6",
}
@InCollection{ Wand85b,
author = "Wand, Mitchell",
title = "From Interpreter to Compiler: A Representational Derivation",
booktitle = "Workshop on Programs as Data Objects (Copenhagen, 1985)",
publisher = springer,
year = "1985",
editor = "H. Ganzinger and Neil D. Jones",
series = lncs,
volume = "217",
pages = "306--324",
address = springeraddr,
}
@InProceedings{ Wand86,
author = "Wand, Mitchell",
title = "Finding the Source of Type Errors",
booktitle = "{\popl{13th}}",
year = "1986",
pages = "38--43",
}
@Article{ Wand87a,
author = "Wand, Mitchell",
title = "A Simple Algorithm and Proof for Type Inference",
journal = "Fundamenta Informaticae",
year = "1987",
volume = "10",
pages = "115--122",
}
@InProceedings{ Wand87b,
author = "Wand, Mitchell",
title = "Complete Type Inference for Simple Objects",
booktitle = "{\lics{2nd}}",
year = "1987",
pages = "37--44",
}
@Manual{ Wand89SPS,
title = "SPS Reference Manual (SPS Version 1.4 (Chez Scheme Version))",
author = "Wand, Mitchell",
year = "1989",
month = apr,
}
@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,
}
@Article{ Wand89b,
author = "Wand, Mitchell",
title = "A Short Proof of the Lexical Addressing Algorithm",
journal = "Information Processing Letters",
year = "1990",
volume = "35",
pages = "1--5",
}
@InProceedings{ Wand89lics,
author = "Wand, Mitchell",
title = "Type Inference for Record Concatenation and Multiple Inheritance",
booktitle = "{\lics{4th}}",
year = "1989",
pages = "92--97",
}
@TechReport{ Wand89objects,
author = "Wand, Mitchell",
title = "Type Inference for Objects with Instance Variables and
Inheritance",
institution = "Northeastern University College of Computer Science",
year = "1989",
type = "Technical Report",
number = "NU-CCS-89-2",
address = "Boston, MA",
month = feb,
}
@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",
}
@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."
}
@Inproceedings{ Wand94objects,
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." }
@Inproceedings{ Wand95,
author = "Mitchell Wand",
title = "Compiler Correctness for Parallel Compilers",
booktitle = "Functional Programming Languages and Computer
Architecture",
pages = "120-134",
year = "1995",
month = jun,
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",
}
@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/}
}
@Article{ WandClinger01,
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{ 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{ 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",
}
@InProceedings{ WandFriedman87,
author = "Wand, Mitchell and Friedman, Daniel P.",
title = "The Mystery of the Tower Revealed: A Non-Reflective
Description of the Reflective Tower",
booktitle = "{\lfp{1986}}",
year = "1986",
pages = "298--307",
note = "Revised version to appear in {\it Lisp and Symbolic
Computation 1} (1988)"
}
@Article{ WandFriedman88,
author = "Wand, Mitchell and Friedman, Daniel P.",
title = "The Mystery of the Tower Revealed: A Non-Reflective
Description of the Reflective Tower",
journal = "Lisp and Symbolic Computation",
year = "1988",
volume = "1",
pages = "11--37",
note = "Reprinted in {\it Meta-Level Architectures and
Reflection} (P. Maes and D. Nardi, eds.) North-Holland, Amsterdam, 1988, pp. 111--134",
}
@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 = {}
}
@Article{ WandKiczalesDutchyn:toplas04,
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},
OPTmonth = {},
pages = {890-910},
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.},
}
@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,
}
@InProceedings{ WandOKeefe89,
author = "Wand, Mitchell and O'Keefe, Patrick",
title = "On the Complexity of Type Inference with Coercion",
booktitle = "Conference on Functional Programming Languages and Computer Architecture",
year = "1989",
address = "London",
month = sep,
}
@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,
}
@InCollection{ WandOKeefeDimen,
author = "Wand, Mitchell and Patrick O'Keefe",
title = "Automatic Dimensional Analysis",
booktitle = "Computational Logic: in honor of J. Alan Robinson",
year = "1991",
editor = "J.-L.~Lassez and Gordon D. Plotkin",
publisher = "MIT Press",
address = "Cambridge, MA",
pages = "479--486"
}
@InProceedings{ WandOliva92,
author = "Mitchell Wand and Dino P. Oliva",
title = "Proving the Correctness of Storage Representations",
booktitle = "{\lfp{1992}}",
year = "1992",
pages = "151--160",
}
@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}
}
@InProceedings{ WandSteckler94a,
author = "Mitchell Wand and Paul Steckler",
title = "Selective, Lightweight Closure Conversion",
booktitle = "{\popl{21st}}",
year = 1994,
OPTeditor = "",
pages = "435-445",
OPTorganization = "",
OPTpublisher = "",
OPTaddress = "",
OPTmonth = "",
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.",
note = "Revised version submitted for publication.",
URL = "ftp://ftp.ccs.neu.edu:pub/wand/papers/popl-94.dvi",
}
@InCollection{ WandSteckler94b,
author = "Michell 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},
}
@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."
}
@InProceedings{ WandSullivan97,
author = {Mitchell Wand and Gregory T. Sullivan},
title = {Denotational Semantics Using an Operationally-Based
Term Model},
booktitle = popl24,
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/},
}
@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{ WandWang90,
author = "Wand, Mitchell and Wang, Zheng-Yu",
title = "Conditional Lambda-Theories and the Verification
of Static Properties of Programs",
booktitle = "{\lics{5th}}",
year = "1990",
pages = "321--332",
}
@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",
OPTnumber = "",
OPTpages = "253-277",
OPTmonth = "",
note = "Preliminary version appeared in {\lics{5th}}, 1990,
pp.~321-332.",
}
@InProceedings{ WandWilliamson02,
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, 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},
}
@Article{ WarmerKleppe99:OCL,
author = {Jos Warmer and Anneke Kleppe},
title = {{OCL}: The constraint language of the {UML}},
journal = { Journal of Object-Oriented Programming},
year = {1999},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
month = may,
OPTpages = {},
OPTnote = {},
OPTURL = {},
OPTabstract = {},
OPTsource = {},
OPTannote = {}
}
@TechReport{ Warren83,
author = "David H. D. Warren",
title = "{An Abstract PROLOG Instruction Set}",
institution = "Artificial Intelligence Center, Computer Science and
Technology Division",
year = "1983",
type = "Technical Report",
number = "309",
address = "SRI International, Menlo Park, CA",
month = oct,
descr = "pllog",
}
@Article{ Wegbreit76,
author = "Wegbreit, Ben",
title = "Goal-Directed Program Transformation",
journal = "IEEE Transactions on Software Engi\-neer\-ing",
year = "1976",
volume = "SE-2",
pages = "69--79",
}
@Article{ WegbreitSpitzen76,
author = "Wegbreit, Ben and Spitzen, Jay M.",
title = "Proving Properties of Complex Data Structures",
journal = "Journal of the ACM",
year = "1976",
volume = "23",
pages = "389--396",
}
@TechReport{ Weinreb81,
author = "D. Weinreb and D. A. Moon",
title = "Flavors: Message Passing in the {LISP} Machine",
institution = "Massachusetts Institute of Technology, A.I. Lab.",
address = "Cambridge, Massachusetts",
type = "A. I. Memo",
number = "602",
keywords = "LISP",
year = "1981",
}
@inproceedings{ WeiseCrew:pldi93programmable,
author = "Daniel Weise and Roger F. Crew",
title = "Programmable Syntax Macros",
booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
pages = "156-165",
year = "1993",
url = "citeseer.ist.psu.edu/weise93programmable.html"
}
@Article{ Weiser84,
author = "Weiser, Mark",
title = "Program Slicing",
journal = "IEEE Transactions on Software Engineering",
volume = "10",
number = "4",
pages = "352-357",
month = "August",
year = 1984}
@Book{ Weissman66,
author = "Weissman, C.",
title = "LISP 1.5 Primer",
publisher = "Dickenson Publishing Co.",
year = "1966",
address = "Encino, CA",
}
@inproceedings{ WelshSolsonaGlover:scheme-unit-ql,
author = "Noel Welsh and Francisco Solsona and Ian Glover",
title = "{S}cheme{U}nit and {S}cheme{QL}",
booktitle = "Proceedings of the Third Workshop on Scheme and
Functional Programming",
month = oct,
year = 2002,
pages = "21--30"
}
@Article{ Wensley58,
author = "Wensley, J. H",
title = "A Class of Non-Analytical Iterative Processes",
journal = "Computer Journal",
year = "1958",
volume = "1",
pages = "163--167",
}
}
Wand, M. and O'Keefe, P.M. ``Type Inference for Partial Types is Decidable,''
{\it {European Symposium on Programming '92}\/} (B. Krieg-Br\"uckner, ed.),
Springer Lecture Notes in Computer Science, Vol.~582, pp. 408--417.
@Book{ Wilkes66,
author = "Wilkes, Maurice V.",
title = "A Short Introduction to Numerical Analysis",
publisher = "Cambridge University Press",
year = "1966",
address = "Cambridge, England",
}
@Book{ Winskel93,
author = "Glynn Winskel",
title = "The Formal Semantics of Programming Languages",
publisher = "MIT Press",
year = "1993",
OPTeditor = "",
OPTvolume = "",
OPTseries = "",
address = "Cambridge, MA",
OPTedition = "",
OPTmonth = "",
OPTnote = ""
}
``Selective and Lightweight Closure Conversion,'' (with P. Steckler), {\it
Conf. Rec. 21th ACM Symp. on Principles of Prog. Lang.\/} (1994), 435--445.
@Book{ WinstonHorn81,
author = "Winston, Patrick H. and Horn, Berthold K. P.",
title = "LISP",
publisher = "Addison-Wesley",
year = "1981",
address = "Reading, MA",
}
@Article{ Wirth71,
author = "Wirth, Niklaus",
title = "Program development by stepwise refinement",
journal = "Communications of the ACM",
year = "1971",
volume = "14",
pages = "221--227",
}
@Book{ Wirth73,
author = "Wirth, Niklaus",
title = "Systematic Programming: An Introduction",
publisher = "Prentice-Hall",
year = "1973",
address = "Englewood Cliffs, NJ",
}
@Article{ Wirth74,
author = "Wirth, Niklaus",
title = "On the Composition of Well-Structured Programs",
journal = "Computing Surveys",
year = "1974",
volume = "6",
pages = "247--259",
}
@Book{ Wirth76,
author = "Wirth, Niklaus",
title = "Algorithms + Data Structures = Programs",
publisher = "Prentice-Hall",
year = "1976",
address = "Englewood Cliffs, NJ",
}
@Article{ Wirth77,
author = "Wirth, Niklaus",
title = "Modula: a Language for Modular Multiprogramming",
journal = "Software-Practice and Experience",
year = "1977",
volume = "7",
pages = "3--35",
}
@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",
}
@InProceedings{ WrightEtAl76,
author = "Wright, Jesse B. and Thatcher, James W. and Wagner,
Eric G. and Goguen, Joseph A.",
title = "Rational Algebraic Theories and Fixed Point Solutions",
booktitle = "Procdeedings 17th IEEE Symposium on Foundations of Comput\-ing",
year = "1976",
pages = "147--158",
}
@article{ WrightFelleisen94,
author = "Andrew K. Wright and Matthias Felleisen",
title = "A Syntactic Approach to Type Soundness",
journal = "Information and Computation",
volume = "115",
number = "1",
pages = "38-94",
year = "1994",
url = "citeseer.nj.nec.com/wright92syntactic.html" }
@Article{ WulfEtAl71,
author = "Wulf, William A. and Russell, D. B. and Habermann, A. N.",
title = "{BLISS}: A Language for Systems Programming",
journal = "Communications of the ACM",
year = "1971",
volume = "14",
pages = "780--790",
}
@Article{ WulfEtAl74,
author = "Wulf, W. A. and others",
title = "{HYDRA}: The Kernel of a Multiprocessor Operating System",
journal = "Communications of the ACM",
year = "1974",
volume = "17",
pages = "337--345",
}
@Book{ WulfEtAl75,
author = "Wulf, W. A. and Johnson, R. K. and Weinstock, C. B. and Hobbs,
S. O. and Geshke, C. M.",
title = "The Design of an Optimizing Compiler",
publisher = "American Elsevier",
year = "1975",
address = "New York",
}
@Article{ WulfEtAl77,
author = "Wulf, W. A. and London, Ralph L. and Shaw, Mary",
title = "Abstraction and Verification in Alphard: Defining and
Specifying Iteration and Generators",
journal = "Communications of the ACM",
year = "1977",
volume = "20",
pages = "553--564",
}
@Book{ Yousse64,
author = "Yousse, B. K.",
title = "Mathematical Induction",
publisher = "Prentice-Hall",
year = "1964",
address = "Englewood Cliffs, NJ",
}
@InProceedings{ Zhangetal94,
author = "Cui Zhang and Rob Shaw and Mark R. Heckman and Gregory D.
Benson and Myla Archer and Karl Levitt and Ronald A. Olsson",
title = "Towards a Formal Verification of a Secure Distributed System
and its Applications",
booktitle = "Proceedings of the 17th National
Computer Security Conference",
address = "Baltimore",
pages = "103-113",
year = "1994",
month = oct,
}
Jos Warmer and Anneke Kleppe. OCL: The constraint language of the UML. Journal of Object-Oriented Programming, may 1999. 13
@Unpublished{ Zhangetal95,
author = "Cui Zhang and Brian R. Becker and Mark R. Heckman
and Karl Legitt and Ron A. Olsson",
title = "A Hierarchical Method for Reasoning about Distributed
Programming Languages and its Applications",
note = "submitted for publication",
address = "Department of Computer Science, University of
California at Davis",
year = "1995",
OPTmonth = ""
}
@TechReport{ ZillesLucasThatcher82,
author = "Zilles, Steven N. and Lucas, P. and Thatcher, James W.",
title = "A Look at Algebraic Specifications",
institution = "IBM",
year = "1982",
type = "Research Report",
number = "RJ 3568",
month = aug,
}
@inproceedings{ ZwiersEtAl:ICALP85,
author = {Job Zwiers and Willem P. de Roever and Peter van Emde Boas},
title = {Compositionality and Concurrent Networks: Soundness and Completeness of a Proofsystem},
booktitle = {Proceedings of the 12th Colloquium on Automata, Languages and Programming},
year = {1985},
isbn = {3-540-15650-X},
pages = {509--519},
publisher = {Springer-Verlag},
address = {London, UK},
}
@Article{ deBakker76,
author = "deBakker, J. W.",
title = "Least Fixed Points Revisited",
journal = "Theoretical Computer Science",
year = "1976",
volume = "2",
pages = "155--182",
}
@Article{ deBakkerMeertens75,
author = "deBakker, J. W. and Meertens, L .G. L. T.",
title = "On the Completeness of the Induction Assertion Method",
journal = "Journal of Computer and Systems Science",
year = "1975",
volume = "11",
pages = "323--357",
}
@inproceedings{ deMeuter97,
author = "W. DeMeuter",
title = "Monads as a theoretical foundation for {AOP}",
booktitle = "International Workshop on Aspect-Oriented Programming at ECOOP",
pages = "25",
year = "1997",
url = "citeseer.nj.nec.com/demeuter97monads.html" }
@proceedings{icalp05,
editor = {Lu\'{\i}s Caires and
Giuseppe F. Italiano and
Lu\'{\i}s Monteiro and
Catuscia Palamidessi and
Moti Yung},
title = {Automata, Languages and Programming, 32nd International
Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005,
Proceedings},
booktitle = {ICALP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3580},
year = {2005},
isbn = {3-540-27580-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@TechReport{vonNeumann45,
author = {John von Neumann},
title = {First Draft of a Report on the EDVAC},
institution = {Moore School of Electrical Engineering, University
of Pennsylvania},
year = 1945
}
@Article{ MeunierEtAl:HOSC-05,
author = {Philippe Meunier and Robby Findler and Paul
A. Steckler and Mitchell Wand},
title = {Selectors Make Analyzing Case-Lambda Too Hard},
journal = {Higher-Order and Symbolic Computation},
year = {2005},
OPTkey = {},
volume = {18},
number = {3-4},
pages = {245-269},
month = dec,
OPTnote = {},
OPTannote = {},
URL = ftpdir # {hosc-05.pdf},
abstract = {Flanagan's set-based analysis (SBA) uses
selectors to choose data flowing through
expressions. For example, the rng selector chooses
the ranges of procedures flowing through an
expression. The MrSpidey static debugger for PLT
Scheme is based on Flanagan's formalism. In PLT
Scheme, a case-lambda is a procedure with possibly
several argument lists and clauses. When a
case-lambda is applied at a particular call site, at
most one clause is actually invoked, chosen by the
number of actual arguments. Therefore, an analysis
should propagate data only through appropriate
case-lambda clauses. MrSpidey propagates data
through all clauses of a case-lambda, lessening its
usefulness as a static debugger. Wishing to retain
Flanagan's framework, we extended it to better
analyze case-lambda with rest parameters by
annotating selectors with arity information. The
resulting analysis gives strictly better results
than MrSpidey. Unfortunately, the improved analysis
is too expensive because of overheads imposed by the
use of selectors. Nonetheless, a closure-analysis
style SBA (CA-SBA) eliminates these overheads and can
give comparable results within cubic time.},
source = {papers/scheme-01},
}
@InProceedings{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 = {}
}
@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{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 = {}
}
@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.},
}
@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. }
}
@article{ Culpepper2010:SCP,
author = {Culpepper, Ryan and Felleisen, Matthias},
title = {Debugging hygienic macros},
journal = {Sci. Comput. Program.},
volume = {75},
issue = {7},
month = {July},
year = {2010},
issn = {0167-6423},
pages = {496--515},
numpages = {20},
url = {http://dx.doi.org/10.1016/j.scico.2009.06.001},
doi = {http://dx.doi.org/10.1016/j.scico.2009.06.001},
acmid = {1773163},
publisher = {Elsevier North-Holland, Inc.},
address = {Amsterdam, The Netherlands, The Netherlands},
keywords = {Debugging, Macros, Scheme, Syntactic abstraction},
}