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