%%% -*-BibTeX-*-
%%% ====================================================================
%%%  BibTeX-file{
%%%     author-1        = "Preston Briggs",
%%%     author-2        = "Nelson H. F. Beebe",
%%%     version         = "2.61",
%%%     date            = "14 April 2007",
%%%     time            = "11:16:31 MDT",
%%%     filename        = "toplas.bib",
%%%     address-1       = "Tera Computer Company
%%%                        2815 Eastlake East
%%%                        Seattle, WA 98102
%%%                        USA",
%%%     address-2       = "University of Utah
%%%                        Department of Mathematics, 110 LCB
%%%                        155 S 1400 E RM 233
%%%                        Salt Lake City, UT 84112-0090
%%%                        USA",
%%%     telephone-1     = "+1 206 325-0800",
%%%     telephone-2     = "+1 801 581 5254",
%%%     FAX-2           = "+1 801 581 4148",
%%%     URL-2           = "http://www.math.utah.edu/~beebe",
%%%     checksum        = "64522 27907 136761 1334879",
%%%     email-1         = "preston at tera.com (Internet)",
%%%     email-2         = "beebe at math.utah.edu, beebe at acm.org,
%%%                        beebe at computer.org (Internet)",
%%%     codetable       = "ISO/ASCII",
%%%     keywords        = "bibliography, BibTeX, ACM Transactions on
%%%                        Programming Languages and Systems, TOPLAS",
%%%     license         = "public domain",
%%%     supported       = "yes",
%%%     docstring       = "This is a COMPLETE bibliography of the journal
%%%                        ACM Transactions on Programming Languages and
%%%                        Systems (CODEN ATPSDT, ISSN 0164-0925),
%%%                        informally known as TOPLAS, covering volumes
%%%                        1--21 (1988--1999).
%%%
%%%                        The publisher maintains a World Wide Web site
%%%                        for this journal at
%%%
%%%                            http://www.acm.org/pubs/contents/journals/toplas/
%%%
%%%                        At version 2.61, the year coverage looked
%%%                        like this:
%%%
%%%                             1979 (  20)    1989 (  30)    1999 (  32)
%%%                             1980 (  33)    1990 (  28)    2000 (  28)
%%%                             1981 (  28)    1991 (  30)    2001 (  14)
%%%                             1982 (  39)    1992 (  22)    2002 (  21)
%%%                             1983 (  36)    1993 (  32)    2003 (  20)
%%%                             1984 (  34)    1994 (  66)    2004 (  28)
%%%                             1985 (  34)    1995 (  39)    2005 (  33)
%%%                             1986 (  26)    1996 (  29)    2006 (  27)
%%%                             1987 (  27)    1997 (  35)    2007 (  13)
%%%                             1988 (  32)    1998 (  34)
%%%
%%%                             Article:        869
%%%                             TechReport:       1
%%%
%%%                             Total entries:  870
%%%
%%%                        This bibliography was initially constructed
%%%                        by hand by the first author (PB) from
%%%                        various sources, and at its last release in
%%%                        February 1995, had 447 entries.
%%%
%%%                        It was further extended by the second
%%%                        author (NHFB) using bibliographies in
%%%                        NHFB's personal files, from the OCLC
%%%                        Contents1st database, from the IEEE INSPEC
%%%                        database, from the computer graphics
%%%                        bibliography archive at ftp.siggraph.org,
%%%                        and from the computer science bibliography
%%%                        collection on ftp.ira.uka.de in
%%%                        /pub/bibliography to which many people of
%%%                        have contributed.  The snapshot of this
%%%                        collection was taken on 5-May-1994, and it
%%%                        consists of 441 BibTeX files, 2,672,675
%%%                        lines, 205,289 entries, and 6,375
%%%                        <at>String{} abbreviations, occupying
%%%                        94.8MB of disk space.  This work updated 85
%%%                        existing entries and added 104 new entries,
%%%                        completing coverage to for all issues up to
%%%                        Volume 17, Number 5, September 1995.
%%%
%%%                        Numerous errors in the sources noted above
%%%                        have been corrected.  Spelling has been
%%%                        verified with the UNIX spell and GNU ispell
%%%                        programs using the exception dictionary
%%%                        stored in the companion file with extension
%%%                        .sok.
%%%
%%%                        The ACM maintains Web pages with journal
%%%                        tables of contents for 1985--1995 at
%%%                        http://www.acm.org/pubs/toc.  That data has
%%%                        been automatically converted to BibTeX
%%%                        form, corrected for spelling and page
%%%                        number errors, and merged into this file.
%%%
%%%                        ACM copyrights explicitly permit abstracting
%%%                        with credit, so article abstracts, keywords,
%%%                        and subject classifications have been
%%%                        included in this bibliography wherever
%%%                        available.  Article reviews have been
%%%                        omitted, until their copyright status has
%%%                        been clarified.
%%%
%%%                        bibsource keys in the bibliography entries
%%%                        below indicate the entry originally came
%%%                        from the computer science bibliography
%%%                        archive, even though it has likely since
%%%                        been corrected and updated.
%%%
%%%                        URL keys in the bibliography point to
%%%                        World Wide Web locations of additional
%%%                        information about the entry.
%%%
%%%                        BibTeX citation tags are uniformly chosen as
%%%                        name:year:abbrev, where name is the family
%%%                        name of the first author or editor, year is a
%%%                        4-digit number, and abbrev is a 3-letter
%%%                        condensation of important title
%%%                        words. Citation tags were automatically
%%%                        generated by software developed for the
%%%                        BibNet Project.
%%%
%%%                        In this bibliography, entries are sorted in
%%%                        publication order, using bibsort -byvolume.
%%%
%%%                        The checksum field above contains a CRC-16
%%%                        checksum as the first value, followed by the
%%%                        equivalent of the standard UNIX wc (word
%%%                        count) utility output of lines, words, and
%%%                        characters.  This is produced by Robert
%%%                        Solovay's checksum utility.",
%%%  }
%%% ====================================================================

@Preamble{
    "\hyphenation{
        Fa-la-schi
        Her-men-e-gil-do
        Lu-ba-chev-sky
        Pu-ru-sho-tha-man
        Roe-ver
        Ros-en-krantz
        Ru-dolph
    }" #
    "\ifx \undefined \circled \def \circled #1{(#1)}\fi" #
    "\ifx \undefined \reg \def \reg {\circled{R}}\fi"
}

%%% ====================================================================
%%% Acknowledgement abbreviations:

@String{ack-meo =  "Melissa E. O'Neill,
                    School of Computing Science,
                    Simon Fraser University,
                    Burnaby, BC,
                    Canada V5A 1S6,
                    e-mail: \path|oneill@cs.sfu.ca|,
                    URL: \path|http://www.cs.sfu.ca/people/GradStudents/oneill/|"}

@String{ack-nhfb = "Nelson H. F. Beebe,
                    University of Utah,
                    Department of Mathematics, 110 LCB,
                    155 S 1400 E RM 233,
                    Salt Lake City, UT 84112-0090, USA,
                    Tel: +1 801 581 5254,
                    FAX: +1 801 581 4148,
                    e-mail: \path|beebe@math.utah.edu|,
                            \path|beebe@acm.org|,
                            \path|beebe@computer.org| (Internet),
                    URL: \path|http://www.math.utah.edu/~beebe/|"}

@String{ack-pb =    "Preston Briggs,
                     Tera Computer Company,
                     2815 Eastlake East,
                     Seattle, WA 98102,
                     USA,
                     Tel: +1 206 325-0800,
                     e-mail: \path|preston@tera.com|"}

%%% ====================================================================
%%% Journal abbreviations:

@String{j-TOPLAS                = "ACM Transactions on Programming
                                  Languages and Systems"}

%%% ====================================================================
%%% Bibliography entries:

@TechReport{Morgan:1988:RC,
  author =       "C. C. Morgan and K. A. Robinson and P. H. B.
                 Gardiner",
  title =        "On the Refinement Calculus",
  type =         "Technical Monograph",
  number =       "PRG-70",
  institution =  "Oxford University Computing Laboratory",
  address =      "Wolfson Building, Parks Road, Oxford, UK",
  month =        oct,
  year =         "1988",
  ISBN =         "0-902928-52-X",
  length =       "151",
}

@Article{Lindstrom:1979:BGC,
  author =       "Gary Lindstrom",
  title =        "Backtracking in a Generalized Control Setting",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "8--26",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Dewar:1979:PRE,
  author =       "Robert B. K. Dewar and Arthur Grand and Ssu-Cheng Liu
                 and Jacob T. Schwartz and Edmond Schonberg",
  title =        "Programming by Refinement, as Exemplified by the
                 {SETL} Representation Sublanguage",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "27--49",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Sites:1979:CLI,
  author =       "Richard L. Sites",
  title =        "The Compilation of Loop Induction Expressions",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "50--57",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Ghezzi:1979:IP,
  author =       "Carlo Ghezzi and Dino Mandrioli",
  title =        "Incremental Parsing",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "58--70",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 6 11:06:56 1996",
  acknowledgement = ack-pb,
}

@Article{Robertson:1979:CGS,
  author =       "Edward L. Robertson",
  title =        "Code Generation and Storage Allocation for Machines
                 with Span-Dependent Instructions",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "71--83",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Lamport:1979:NAP,
  author =       "Leslie Lamport",
  title =        "A New Approach to Proving the Correctness of
                 Multiprocess Programs",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "84--97",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 6 13:02:18 1996",
  note =         "See also corrigendum \cite{Lamport:1980:CNA}.",
  acknowledgement = ack-pb,
}

@Article{Constable:1979:HAF,
  author =       "Robert L. Constable and James E. Donahue",
  title =        "A Hierarchical Approach to Formal Semantics With
                 Application to the Definition of {PL\slash CS}",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "98--114",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Fri Jan 5 18:36:35 1996",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Wise:1979:MGC,
  author =       "David S. Wise",
  title =        "{Morris}'s Garbage Compaction Algorithm Restores
                 Reference Counts",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "115--120",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Lengauer:1979:FAF,
  author =       "Thomas Lengauer and Robert Endre Tarjan",
  title =        "A Fast Algorithm for Finding Dominators in a
                 Flowgraph",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "121--141",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Kennedy:1979:DAG,
  author =       "Ken Kennedy and Jayashree Ramanathan",
  title =        "A Deterministic Attribute Grammar Evaluator Based on
                 Dynamic Scheduling",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "1",
  pages =        "142--160",
  month =        jul,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Parallel/scheduling.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  acknowledgement = ack-pb,
}

@Article{Iverson:1979:O,
  author =       "Kenneth E. Iverson",
  title =        "Operators",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "161--176",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Perrott:1979:LAV,
  author =       "R. H. Perrott",
  title =        "A Language for Array and Vector Processors",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "177--195",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Prywes:1979:UNS,
  author =       "N. S. Prywes and Amir Pnueli and S. Shastry",
  title =        "Use of a Nonprocedural Specification Language and
                 Associated Program Generator in Software Development",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "196--217",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Kieburtz:1979:CCS,
  author =       "Richard B. Kieburtz and Abraham Silberschatz",
  title =        "Comments on ``{Communicating} Sequential Processes''",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "218--225",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Luckham:1979:VAR,
  author =       "David C. Luckham and Norihisa Suzuki",
  title =        "Verification of Array, Record, and Pointer Operations
                 in {Pascal}",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "226--244",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Nelson:1979:SCD,
  author =       "Greg Nelson and Derek C. Oppen",
  title =        "Simplification by Cooperating Decision Procedures",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "245--257",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib,
                 Ai/Constr.logic.prog.bib",
  acknowledgement = ack-pb,
}

@Article{Gries:1979:SEB,
  author =       "David Gries",
  title =        "Is Sometimes Ever Better Than Alway?",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "258--265",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Bobrow:1979:CEL,
  author =       "Daniel G. Bobrow and Douglas W. Clark",
  title =        "Compact Encodings of List Structure",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "266--286",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/Heaps.bib, Compiler/garbage.collection.bib,
                 Compiler/Compiler.Lins.bib, Compiler/TOPLAS.bib",
  acknowledgement = ack-pb,
  comment =      "Good words on {CDR}-coding",
}

@Article{Beyer:1979:SED,
  author =       "Eric Beyer and Peter Buneman",
  title =        "A Space Efficient Dynamic Allocation Algorithm for
                 Queuing Messages",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "287--294",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Tai:1979:NSG,
  author =       "Kou-Chung Tai",
  title =        "Noncanonical {SLR}(1) Grammars",
  journal =      j-TOPLAS,
  volume =       "1",
  number =       "2",
  pages =        "295--320",
  month =        oct,
  year =         "1979",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Harel:1980:PNA,
  author =       "David Harel",
  title =        "{And/Or} Programs: {A} New Approach to Structured
                 Programming",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "1--17",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Pai:1980:GCR,
  author =       "Ajit B. Pai and Richard B. Kieburtz",
  title =        "Global Context Recovery: {A} New Strategy for
                 Syntactic Error Recovery by Table-Drive Parsers",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "18--41",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Francez:1980:DT,
  author =       "Nissim Francez",
  title =        "Distributed Termination",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "42--55",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 13:02:21 1996",
  note =         "See also corrigendum \cite{Francez:1980:CT} and
                 remarks \cite{Mohan:1981:TCF,Francez:1981:TCR}.",
  acknowledgement = ack-pb,
}

@Article{Andrews:1980:AAI,
  author =       "Gregory R. Andrews and Richard P. Reitman",
  title =        "An Axiomatic Approach to Information Flow in
                 Programs",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "56--76",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Papadimitriou:1980:PBH,
  author =       "Christos H. Papadimitriou and Philip A. Bernstein",
  title =        "On the Performance of Balanced Hashing Functions When
                 the Keys Are Not Equiprobable",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "77--89",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Misc/hash.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  acknowledgement = ack-pb,
}

@Article{Manna:1980:DAP,
  author =       "Zohar Manna and Richard Waldinger",
  title =        "A Deductive Approach to Program Synthesis",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "90--121",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Arnold:1980:URG,
  author =       "D. B. Arnold and M. R. Sleep",
  title =        "Uniform Random Generation of Balanced Parenthesis
                 Strings",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "122--128",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Comer:1980:NMS,
  author =       "Douglas Comer",
  title =        "A Note on Median Split Trees",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "129--133",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Lamport:1980:CNA,
  author =       "Leslie Lamport",
  title =        "Corrigendum: ``{A New Approach to Proving the
                 Correctness of Multiprocess Programs}''",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "1",
  pages =        "134--134",
  month =        jan,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 12:53:34 1996",
  note =         "See \cite{Lamport:1979:NAP}.",
  acknowledgement = ack-pb,
}

@Article{Wallis:1980:ERO,
  author =       "Peter J. L. Wallis",
  title =        "External Representations of Objects of User-Defined
                 Type",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "137--152",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  note =         "See also corrigendum \cite{Wallis:1981:CRO}.",
  acknowledgement = ack-pb,
}

@Article{Griswold:1980:AUP,
  author =       "Ralph E. Griswold and David R. Hanson",
  title =        "An Alternative to the Use of Patterns in String
                 Processing",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "153--172",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Cattell:1980:ADC,
  author =       "R. G. G. Cattell",
  title =        "Automatic Derivation of Code Generators from Machine
                 Descriptions",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "173--190",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Davidson:1980:DAR,
  author =       "Jack W. Davidson and Christopher W. Fraser",
  title =        "The Design and Application of a Retargetable Peephole
                 Optimizer",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "191--202",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 13:02:24 1996",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  note =         "See also corrigendum \cite{Davidson:1981:CDA}.",
  acknowledgement = ack-pb,
}

@Article{Fischer:1980:PCA,
  author =       "Charles N. Fischer",
  title =        "On Parsing and Compiling Arithmetic Expressions on
                 Vector Computers",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "203--224",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Luckham:1980:AEH,
  author =       "David C. Luckham and W. Polak",
  title =        "{Ada} exception handling: an axiomatic approach",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "225--233",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/Compiler.Lins.bib, Compiler/TOPLAS.bib",
  acknowledgement = ack-pb,
}

@Article{Bernstein:1980:OGN,
  author =       "Arthur Bernstein",
  title =        "Output Guards and Nondeterminism in ``{Communicating
                 Sequential Processes}''",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "234--238",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Theory/ProbAlgs.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  note =         "Bernstein presents a distributed algorithm for CSP
                 output guards based on priority ordering of
                 processes.",
  acknowledgement = ack-pb,
}

@Article{Ma:1980:DMI,
  author =       "Perng-Ti Ma and T. G. Lewis",
  title =        "Design of a Machine-Independent Optimizing System for
                 Emulator Development",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "2",
  pages =        "239--262",
  month =        apr,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Bobrow:1980:MRS,
  author =       "Daniel G. Bobrow",
  title =        "Managing Reentrant Structures Using Reference Counts",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "269--273",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Leverett:1980:CSD,
  author =       "Bruce W. Leverett and Thomas G. Szymanski",
  title =        "Chaining Span-Dependent Jump Instructions",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "274--289",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Samet:1980:CAP,
  author =       "Hanan Samet",
  title =        "A Coroutine Approach to Parsing",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "290--306",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Howden:1980:ASV,
  author =       "W. E. Howden",
  title =        "Applicability of Software Validation Techniques to
                 Scientific Programs",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "307--320",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Broy:1980:DIA,
  author =       "Manfred Broy and Bernd Krieg-{Br\"uckner}",
  title =        "Derivation of Invariant Assertions During Program
                 Development by Transformation",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "321--337",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Clarke:1980:SRI,
  author =       "Edmund Melson {Clarke, Jr.}",
  title =        "Synthesis of Resource Invariants for Concurrent
                 Programs",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "338--358",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Apt:1980:PSC,
  author =       "Krzysztof R. Apt and Nissim Francez and Willem P. de
                 Roever",
  title =        "A Proof System for Communicating Sequential
                 Processes",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "359--385",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 6 13:22:43 1996",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  note =         "See remarks \cite{Moitra:1983:TCA}.",
  acknowledgement = ack-pb,
}

@Article{Casanova:1980:FSR,
  author =       "Marco R. Casanova and Phillip A. Bernstein",
  title =        "A Formal System for Reasoning about Programs Accessing
                 a Relational Database",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "386--414",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Graham:1980:ICF,
  author =       "Susan L. Graham and Michael A. Harrison and Walter L.
                 Ruzzo",
  title =        "An Improved Context-Free Recognizer",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "415--462",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Francez:1980:CT,
  author =       "Nissim Francez",
  title =        "Corrigendum: ``{Distributed Termination}''",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "3",
  pages =        "463--463",
  month =        jul,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 12:55:53 1996",
  note =         "See
                 \cite{Francez:1980:DT,Mohan:1981:TCF,Francez:1981:TCR}.",
  acknowledgement = ack-pb,
}

@Article{Oppen:1980:P,
  author =       "Dereck C. Oppen",
  title =        "Prettyprinting",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "4",
  pages =        "465--483",
  month =        oct,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Schwartz:1980:U,
  author =       "Jacob T. Schwartz",
  title =        "Ultracomputers",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "4",
  pages =        "484--521",
  month =        oct,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Ernst:1980:SAD,
  author =       "George W. Ernst and William F. Ogden",
  title =        "Specification of Abstract Data Types in {Modula}",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "4",
  pages =        "522--543",
  month =        oct,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Landwehr:1980:ATS,
  author =       "Carl E. Landwehr",
  title =        "An Abstract Type for Statistics Collection in
                 {Simula}",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "4",
  pages =        "544--563",
  month =        oct,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Gries:1980:APC,
  author =       "David Gries and Gary Levin",
  title =        "Assignment and Procedure Call Proof Rules",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "4",
  pages =        "564--579",
  month =        oct,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Moret:1980:AVR,
  author =       "B. M. E. Moret and M. G. Thomason and R. C. Gonzalez",
  title =        "The Activity of a Variable and Its Relation to
                 Decision Trees",
  journal =      j-TOPLAS,
  volume =       "2",
  number =       "4",
  pages =        "580--595",
  month =        oct,
  year =         "1980",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Steensgaard-Madsen:1981:SOA,
  author =       "J. Steensgaard-Madsen",
  title =        "A Statement-Oriented Approach to Data Abstraction",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "1--10",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  note =         "See remarks
                 \cite{Ellis:1982:TCS,Steensgaard-Madsen:1982:SMR}.",
  acknowledgement = ack-pb,
}

@Article{Andre:1981:MAC,
  author =       "F. {Andr\'e} and J. P. Banatre and J. P. Routeau",
  title =        "A Multiprocessing Approach to Compile-Time Symbol
                 Resolution",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "11--23",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Juelich:1981:CAS,
  author =       "Otto C. Juelich and Clinton R. Foulk",
  title =        "Compilation of Acyclic Smooth Programs for Parallel
                 Execution",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "24--48",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Grit:1981:DIT,
  author =       "Dale H. Grit and Rex L. Page",
  title =        "Deleting Irrelevant Tasks in an Expression-Oriented
                 Multiprocessor System",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "49--59",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/Heaps.bib, Compiler/garbage.collection.bib,
                 Compiler/Compiler.Lins.bib, Compiler/TOPLAS.bib",
  acknowledgement = ack-pb,
}

@Article{Kristensen:1981:MCL,
  author =       "Bent Bruun Kristensen and Ole Lehrmann Madsen",
  title =        "Methods for Computing {LALR$(k)$} Lookahead",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "60--82",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/Compiler.Lins.bib, Compiler/TOPLAS.bib",
  acknowledgement = ack-pb,
}

@Article{LaLonde:1981:HOP,
  author =       "Wilf R. LaLonde and Jim des Rivieres",
  title =        "Handling Operator Precedence in Arithmetic Expressions
                 with Tree Transformations",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "83--103",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 6 13:17:11 1996",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  note =         "See remarks
                 \cite{Henderson:1983:TCL,LaLonde:1983:TCL}.",
  acknowledgement = ack-pb,
}

@Article{Misra:1981:EPE,
  author =       "Jayadev Misra",
  title =        "An Exercise in Program Explanation",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "104--109",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Davidson:1981:CDA,
  author =       "Jack W. Davidson and Christopher W. Fraser",
  title =        "Corrigendum: ``{The Design and Application of a
                 Retargetable Peephole Optimizer}''",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "110--110",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 12:58:29 1996",
  note =         "See \cite{Davidson:1980:DAR}.",
  acknowledgement = ack-pb,
}

@Article{Wallis:1981:CRO,
  author =       "Peter J. L. Wallis",
  title =        "Corrigendum: ``{External Representations of Objects of
                 User-Defined Type}''",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "111--111",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 12:58:29 1996",
  note =         "See \cite{Wallis:1980:ERO}.",
  acknowledgement = ack-pb,
}

@Article{Mohan:1981:TCF,
  author =       "C. Mohan",
  title =        "Technical Correspondence: On {Francez}'s
                 ``{Distributed Termination}''",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "112--112",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 12:58:29 1996",
  note =         "See \cite{Francez:1980:DT,Francez:1981:TCR}.",
  acknowledgement = ack-pb,
}

@Article{Francez:1981:TCR,
  author =       "N. Francez",
  title =        "Technical Correspondence: Reply from {Francez}",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "1",
  pages =        "112--113",
  month =        jan,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 13:05:53 1996",
  note =         "See \cite{Francez:1980:DT,Mohan:1981:TCF}.",
  acknowledgement = ack-nhfb,
}

@Article{Fraser:1981:EDS,
  author =       "Christopher W. Fraser and A. A. Lopez",
  title =        "Editing Data Structures",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "2",
  pages =        "115--125",
  month =        apr,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib,
                 Ai/lisp.bib",
  acknowledgement = ack-pb,
}

@Article{Schonberg:1981:ATS,
  author =       "Edmond Schonberg and Jacob T. Schwartz and Micha
                 Sharir",
  title =        "An Automatic Technique for Selection of Data
                 Structures in {SETL} Programs",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "2",
  pages =        "126--143",
  month =        apr,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Database/Graefe.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "SETL is a very high level programming language
                 supporting set theoretic syntax and semantics. It
                 allows algorithms to be programmed rapidly and
                 succinctly without requiring data structure
                 declarations to be supplied. Such declarations can be
                 manually specified later, without recoding the program,
                 to improve the efficiency of program execution. We
                 describe a new technique for automatic selection of
                 appropriate data representations during compile time
                 for programs with omitted declarations and present an
                 efficient data representation selection algorithm,
                 whose complexity is comparable with those of the
                 fastest known general data-flow algorithms of Tarjan
                 and Reif.",
  acknowledgement = ack-pb,
  keywords =     "New York Univ. bit vector direct representation
                 pointer array for subsets",
}

@Article{Griswold:1981:GI,
  author =       "Ralph E. Griswold and David R. Hanson and John T.
                 Korb",
  title =        "Generators in {Icon}",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "2",
  pages =        "144--161",
  month =        apr,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Hanson:1981:APP,
  author =       "David R. Hanson",
  title =        "{Algorithm 568}. {PDS} --- {A} Portable Directory
                 System",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "2",
  pages =        "162--167",
  month =        apr,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Fri Sep 9 14:11:06 1994",
  URL =          "http://doi.acm.org/10.1145/357133.357137",
  acknowledgement = ack-pb,
}

@Article{LaLonde:1981:CSC,
  author =       "Wilf R. LaLonde",
  title =        "The Construction of Stack-Controlling {LR} Parsers for
                 Regular Right Part Grammars",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "2",
  pages =        "168--206",
  month =        apr,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Gannon:1981:DAI,
  author =       "John Gannon and Paul McMullin and Richard Hamlet",
  title =        "Data Abstraction, Implementation, Specification, and
                 Testing",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "3",
  pages =        "211--223",
  month =        jul,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{vandenBos:1981:PCB,
  author =       "Jan {van den Bos} and R. Plasmeijer and Jan W. M.
                 Stroet",
  title =        "Process Communication Based on Input Specifications",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "3",
  pages =        "224--250",
  month =        jul,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Fri Oct 31 06:37:56 2003",
  bibsource =    "Object/Nierstrasz.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  acknowledgement = ack-pb,
  keywords =     "uilit",
}

@Article{Rem:1981:APN,
  author =       "Martin Rem",
  title =        "Associons: {A} Program Notation with Tuples Instead of
                 Variables",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "3",
  pages =        "251--262",
  month =        jul,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Lindstrom:1981:RRB,
  author =       "Gary Lindstrom and Mary Lou Soffa",
  title =        "Referencing and Retention in Block-Structured
                 Coroutines",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "3",
  pages =        "263--292",
  month =        jul,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Barnden:1981:NCA,
  author =       "J. A. Barnden",
  title =        "Nonsequentiality and Concrete Activity Phases in
                 Discrete-Event Simulation Languages",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "3",
  pages =        "293--317",
  month =        jul,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Anderson:1981:LLC,
  author =       "S. O. Anderson and R. C. Backhouse",
  title =        "Locally Least-Cost Error Recovery in {Early}'s
                 Algorithm",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "3",
  pages =        "318--347",
  month =        jul,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Borning:1981:PLA,
  author =       "Alan Borning",
  title =        "The Programming Language Aspects of {ThingLab}, a
                 Constraint-Oriented Simulation Laboratory",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "4",
  pages =        "353--387",
  month =        oct,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Jazayeri:1981:SES,
  author =       "Medhi Jazayeri and Diane Pozefsky",
  title =        "Space-Efficient Storage Management in an Attribute
                 Grammar Evaluator",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "4",
  pages =        "388--404",
  month =        oct,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Andrews:1981:SR,
  author =       "Gregory R. Andrews",
  title =        "Synchronizing Resources",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "4",
  pages =        "405--430",
  month =        oct,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Apt:1981:TYH,
  author =       "Krzysztof R. Apt",
  title =        "Ten Years of {Hoare}'s Logic: {A} Survey --- {Part
                 I}",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "4",
  pages =        "431--483",
  month =        oct,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/prog.lang.theory.bib",
  acknowledgement = ack-pb,
}

@Article{Greif:1981:SSW,
  author =       "Irene Greif and Albert R. Meyer",
  title =        "Specifying the Semantics of while Programs: {A}
                 Tutorial and Critique of a Paper by {Hoare} and
                 {Lauer}",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "4",
  pages =        "484--507",
  month =        oct,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/Compiler.Lins.bib",
  acknowledgement = ack-pb,
}

@Article{Hansen:1981:CMI,
  author =       "Wilfred J. Hansen",
  title =        "A Cost Model for the Internal Organization of
                 {B$^{+}$}-Tree Nodes",
  journal =      j-TOPLAS,
  volume =       "3",
  number =       "4",
  pages =        "508--532",
  month =        oct,
  year =         "1981",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Feather:1982:SAP,
  author =       "Martin S. Feather",
  title =        "A System for Assisting Program Transformation",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "1--20",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "Program transformation has been advocated as a
                 potentially appropriate methodology for program
                 development. The ability to transform large programs is
                 crucial to the practicality of such an approach. This
                 paper describes research directed towards applying one
                 particular transformation method to problems of
                 increasing scale. The method adopted is that developed
                 by Burstall and Darlington, and familiarity with their
                 work is assumed. The problems which arise when
                 attempting transformation of larger scale programs are
                 discussed, and an approach to overcoming them is
                 presented. Parts of the approach have been embodied in
                 a machine-based system which assists a user in
                 transforming his programs. The approach, and the use of
                 this system, are illustrated by presenting portions of
                 the transformation of a compiler for a ``toy''
                 language.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "program development; program transformation",
  sjb =          "Manual transformation method i.e. the program has to
                 be told where to do the transformations.",
  source =       "Dept. Library",
}

@Article{Tanenbaum:1982:UPO,
  author =       "Andrew S. Tanenbaum and Hans {van Staveren} and Johan
                 W. Stevenson",
  title =        "Using Peephole Optimization on Intermediate Code",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "21--36",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Mon Oct 26 07:58:22 1998",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  note =         "See remarks \cite{Pemberton:1983:TCT}.",
  abstract =     "Many portable compilers generate an intermediate code
                 that is subsequently translated into target machine's
                 assembly language. In this paper a stack-machine-based
                 intermediate code suitable for algebraic languages
                 (e.g., PASCAL, C, FORTRAN) and most byte-addressed
                 mini- and microcomputers is described. A table-driven
                 peephole optimizer that improves the intermediate code
                 is discussed in detail and compared with other local
                 optimization methods. Measurements show an improvement
                 of about 15 percent, depending on precise metrics
                 used.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "abstract machine; intermediate code; peephole
                 optimizer",
  source =       "Dept. Library",
}

@Article{Misra:1982:TDD,
  author =       "Jayadev Misra and K. M. Chandy",
  title =        "Termination Detection of Diffusing Computations in
                 Communicating Sequential Processes",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "37--43",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "In this paper it is shown how the Dijkstra-Scholten
                 scheme for termination detection in a diffusing
                 computation can be adapted to detect termination or
                 deadlock in a network of communicating sequential
                 processes as defined by Hoare.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "diffusing computation; distributed systems; networks
                 of processes; termination detection",
  source =       "Dept. Library",
}

@Article{McGraw:1982:VLD,
  author =       "James R. McGraw",
  title =        "The {VAL} Language: Description and Analysis",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "44--82",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Parallel/par.dataflow.bib, Misc/Functional.bib,
                 Compiler/Compiler.Lins.bib, Compiler/TOPLAS.bib,
                 Compiler/bevan.bib",
  abstract =     "VAL is a high-level, function-based language designed
                 for use on data flow computers. A data flow computer
                 has many small processors organized to cooperate in the
                 execution of a single computation. A computation is
                 represented by its data flow graph; each operator in a
                 graph is scheduled for execution on one of the
                 processors after all of its operands' values are known.
                 VAL promotes the identification of concurrency in
                 algorithms and simplifies the mapping into data flow
                 graphs. This paper presents a detailed introduction to
                 VAL and analyzes its usefulness for programming in a
                 highly concurrent environment. VAL provides {\em
                 implicit concurrency\/} (operations that can execute
                 simultaneously are evident without the need for any
                 explicit language notation). The language uses
                 function- and expression-based features that prohibit
                 all side effects, which simplifies translation to
                 graphs. The salient language features are described and
                 illustrated through examples taken from a complete VAL
                 program for adaptive quadrature. Analysis of the
                 language shows that VAL meets the critical needs for a
                 data flow environment. The language encourages
                 programmers to think in terms of general concurrency,
                 enhances readability (due to the absence of side
                 effects), and possesses a structure amenable
                 verification techniques. However, VAL is still
                 evolving. The language definition needs refining, and
                 more support tools for programmer use need to be
                 developed. Also, some new kinds of optimization
                 problems should be addressed.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "applicative languages; concurrent programming
                 structures; data-flow languages; design; functional;
                 languages",
  source =       "Dept. Library",
}

@Article{Hoffman:1982:PE,
  author =       "Christoph M. Hoffman and Michael J. O'Donnell",
  title =        "Programming with Equations",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "83--112",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "Equations provide a convenient notation for defining
                 many computations, for example, for programming
                 language interpreters. This paper illustrates the
                 usefulness of equational programs, describes the
                 problems involved in implementing equational programs,
                 and investigates practical solutions to those problems.
                 The goal of the study is a system to automatically
                 transform a set of equations into an efficient program
                 which exactly implements the logical meaning of the
                 equations. This logical meaning may be defined in terms
                 of the traditional mathematical interpretation of
                 equations, without using advanced computing concepts.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "equations; interpreters; nonprocedural languages;
                 term-rewriting systems",
  sjb =          "Includes code for a 2-3 tree.",
}

@Article{Williams:1982:FNS,
  author =       "M. Howard Williams",
  title =        "A Flexible Notation for Syntactic Definitions",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "113--119",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Fri Jun 8 13:21:42 1984",
  bibsource =    "Compiler/compiler.bib, Compiler/bevan.bib",
  abstract =     "In view of the proliferation of notations for defining
                 the syntax of programming languages, it has been
                 suggested that a simple notation should be adopted as a
                 standard. However, any notation adopted as a standard
                 should also be as versatile as possible. For this
                 reason, a notation is presented here which is both
                 simple and versatile and which has additional benefits
                 when specifying the static semantic rules of a
                 language.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "BNF; syntax",
  sjb =          "Suggests some additions to Wirth's notation to capture
                 some commonly required constraints such as ``maximum
                 length of an identifier is $X$'', ``$X$ can be repeated
                 $Y$ times''. The ``simple and versatile'' notation is
                 just Wirth's EBNF augmented with affixes/attributes.
                 Ends with the following ``It is hoped that this paper
                 will not be viewed simply as a presentation of yet
                 another notation for syntactic definitions. The main
                 purpose of the paper has been to look closely at the
                 advantages of the notation proposed, and it is hoped
                 that in the future, before adopting any syntactic
                 notation, readers will give careful consideration to
                 the advantages of such a notation and avoid the
                 introduction of new notations or variations on existing
                 ones unless the advantages can be clearly spelled
                 out.''",
}

@Article{Ellis:1982:TCS,
  author =       "John R. Ellis",
  title =        "Technical Correspondence: On {Steensgaard-Madsen}'s
                 ``{A Statement-Oriented Approach to Data
                 Abstraction}''",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "120--122",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 13:08:12 1996",
  bibsource =    "Compiler/bevan.bib",
  note =         "See
                 \cite{Steensgaard-Madsen:1981:SOA,Steensgaard-Madsen:1982:SMR}",
  checked =      "19940302",
  sjb =          "Points out that Madsen's ``new'' approach already
                 exists in languages like Smalltalk and Scheme.",
}

@Article{Steensgaard-Madsen:1982:SMR,
  author =       "J. Steensgaard-Madsen",
  title =        "Technical Correspondence: {Steensgaard-Madsen}'s
                 reply",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "1",
  pages =        "122--123",
  month =        jan,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  note =         "See
                 \cite{Steensgaard-Madsen:1981:SOA,Ellis:1982:TCS}.",
  checked =      "19940302",
  sjb =          "Admits ignorance of Scheme and Smalltalk, but doggedly
                 clings to the idea that his approach is new.",
}

@Article{Schneider:1982:SDP,
  author =       "Fred B. Schneider",
  title =        "Synchronization in Distributed Programs",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "125--148",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "A technique for solving synchronization problems in
                 distributed programs is described. Use of this
                 technique in environments in which processes may fail
                 is discussed. The technique can be used to solve
                 synchronization problems directly, to implement new
                 synchronization mechanisms (which are presumably well
                 suite for use in distributed programs), and to
                 construct distributed versions of existing
                 synchronization mechanisms. use of the technique is
                 illustrated with implementations of distributed
                 semaphores and a conditional message-passing
                 facility.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "logical clocks",
  source =       "Dept. Library",
}

@Article{Holt:1982:ISS,
  author =       "Richard C. Holt and J. R. Cordy and David B. Wortman",
  title =        "An Introduction to {S/SL}: {Syntax\slash Semantic
                 Language}",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "149--178",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Fri Jan 5 18:36:33 1996",
  bibsource =    "Compiler/bevan.bib, Compiler/TOPLAS.bib,
                 Compiler/Compiler.Lins.bib",
  abstract =     "S/SL (Syntax/Semantic Language) is a language that was
                 developed for implementing compilers. A subset called
                 SL (Syntax Language) has the same recognition power as
                 do LR(k) parsers. Complete S/SL includes invocation of
                 semantic operations implemented in another language
                 such as PASCAL. S/SL implies a top-down programming
                 methodology. First, a data-free algorithm is developed
                 in S/SL. The algorithm invokes operations on ``semantic
                 mechanisms.'' A semantic mechanism is an abstract
                 object, specified, from the point of view of the S/SL,
                 only by the effect of operations upon the object.
                 Later, the mechanisms are implemented apart from the
                 S/SL program. The separation of the algorithm from the
                 data and the division of data into mechanisms reduce
                 the effort needed to understand and maintain the
                 resulting software. S/SL has been used to construct
                 compilers for SPECKLE (a PL/I subset), PT (a PASCAL
                 subset), Toronto EUCLID, and Concurrent EUCLID. It has
                 been used to implement scanners, parser, semantic
                 analyzers, and code generators. S/SL programs are
                 implemented by translating them into tables of
                 integers. A ``table walker'' program executes the S/SL
                 program by interpreting this table. The translation of
                 S/SL programs into tables is performed by a program
                 called the S/SL processor. This processor serves a
                 function analogous to that served by an LR(k) parser
                 generator. The implementation of S/SL is simple and
                 portable. It is available in a small subset of PASCAL
                 that can be easily transliterated into other high-level
                 languages.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "design languages; LR(k)",
  source =       "Dept. Library",
}

@Article{Soisalon-Soininen:1982:IEE,
  author =       "Eljas Soisalon-Soininen",
  title =        "Inessential Error Entries and Their Use in {LR} Parser
                 Optimization",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "179--195",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  note =         "See \cite{LaLonde:1984:TCC}.",
  abstract =     "The use of ``default reductions'' in implementing LR
                 parsers is considered in conjunction with the desire to
                 decrease the number of states of the parser by making
                 use of ``don't care'' (also called ``inessential'')
                 error entries. Default reduction are those which are
                 performed independently of the lookahead string when
                 other operations do not apply, and their use can lead
                 to substantial savings in space and time. Don't-care
                 error entries of an LR parser are those which are never
                 consulted, and thus they can be arbitrarily replaced by
                 nonerror entries in order to make a state compatible
                 with another one. Determining don't-care error entries
                 is most important in avoiding the growth of the sie of
                 the parser when eliminating reductions by single
                 productions, that is, productions for which the
                 right-hand side is a single symbol. The use of default
                 reductions diminishes don't-care entries. This effect
                 is analyzed by giving a necessary and sufficient
                 condition for an error entry to be don't care when
                 default reductions are used. As an application,
                 elimination of reductions by single productions in
                 conjunction with the use of default reductions is
                 considered.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "default reductions; don't-care error entries; LR(k);
                 single productions",
  source =       "Dept. Library",
}

@Article{Sharir:1982:SOC,
  author =       "Micha Sharir",
  title =        "Some Observations Concerning Formal Differentiation of
                 Set Theoretic Expressions",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "196--225",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Wetherell:1982:EDV,
  author =       "C. S. Wetherell",
  title =        "Error Data Values in the Data-Flow Language {VAL}",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "226--238",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "The data-flow architecture is intended to support
                 large scientific computations, and VAL is an algebraic,
                 procedural language for use on a data-flow computer.
                 VAL is Apt for numerical computations but requires an
                 error monitoring feature that can be used to diagnose
                 and correct errors arising during program execution.
                 Traditional monitoring methods (software traps and
                 condition codes) are inappropriate for VAL; instead VAL
                 includes a set of error data values and an algebra for
                 their manipulation. The error data values and their
                 algebra are described an assessed; the conclusion is
                 that error values provide a clean way for a high-level
                 language to handle numeric (and some other) errors.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "applicative languages; computer arithmetic; data-flow
                 architectures; data-flow languages; design; error
                 handling and recovery; languages",
  sjb =          "easy read",
  source =       "Dept. Library",
}

@Article{Fateman:1982:HLL,
  author =       "Richard J. Fateman",
  title =        "High-Level Language Implications of the Proposed
                 {IEEE} Floating-Point Standard",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "239--257",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "An IEEE Computer Society working group on
                 floating-point arithmetic has recommended a standard
                 for binary floating-point number formats, operations,
                 and semantics. This paper, which has evolved in part
                 during the deliberations of that committee, describes
                 the significance to languages and, in particular, to
                 FORTRAN and its variants, of various novel features of
                 the recommended standard.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "computer arithmetic; control structures; data types
                 and structures; error handling and recovery;
                 floating-point arithmetic; FORTRAN; run-time
                 environments",
  source =       "Dept. Library",
}

@Article{Martelli:1982:EUA,
  author =       "Alberto Martelli and Ugo Montanari",
  title =        "An Efficient Unification Algorithm",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "258--282",
  month =        feb,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/prog.lang.theory.bib, Compiler/TOPLAS.bib,
                 Ai/prolog.1.bib, Compiler/Compiler.Lins.bib,
                 Compiler/bevan.bib,
                 Misc/formal.hardware.verification.bib",
  abstract =     "The unification problem in first-order predicate
                 calculus is described in general terms as the solution
                 of a system of equations, and a nondeterministic
                 algorithm is given. A new unification algorithm,
                 characterized by having the acyclicity test efficiently
                 embedded into it, is derived from the nondeterministic
                 one, and a PASCAL implementation is given. A comparison
                 with other well-known unification algorithms shows that
                 the algorithm described here performs well in all
                 cases.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "algorithms; complexity of proof procedures; languages;
                 logic; mechanical theorem proving; performance; prolog;
                 resolution; theory",
  source =       "Dept. Library",
}

@Article{Ashcroft:1982:BRS,
  author =       "E. A. Ashcroft and W. W. Wadge",
  title =        "{\bf R}$_{\!\!\!\mbox{\raisebox{.5ex}{\tiny /}}}$ for
                 Semantics",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "283--294",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "A constructive criticism of recent work in the
                 semantics of programming languages is offered. The
                 criticism is directed not so much at the techniques and
                 results obtained as at the use to which they are put.
                 The fact that denotational (or ``mathematical'')
                 semantics plays on the whole a passive
                 (``descriptive'') role, while operational semantics
                 plays on the whole an active (``prescriptive'') role,
                 is seen as the basic problem. It is suggested that
                 these roles be reversed.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "denotational semantics; operational semantics;
                 semantics; theory",
  sjb =          "Easy read. Note the format of the title is taken the
                 ACM TOPLAS bibliography maintained by
                 preston@cs.rice.edu",
  source =       "Dept. Library",
}

@Article{Arsac:1982:STR,
  author =       "J. Arsac and Y. Kodratoff",
  title =        "Some Techniques for Recursion Removal from Recursive
                 Functions",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "2",
  pages =        "295--322",
  month =        apr,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "Three different techniques that can be used for
                 recursion removal are described: generalization of the
                 function definition, study of the computation traces of
                 the function, and nonprocedural languages. Despite the
                 existence of implemented versions of these techniques,
                 they are easy to use ``by hand'' and should therefore
                 be part of every programmers knowledge.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "computation trace; denotational semantics; operational
                 semantics; recursion removal; semantics; tail
                 recursion",
  sjb =          "Gets a bit heavy in places, but on the whole quite
                 readable.",
  source =       "Dept. Library",
}

@Article{Hennessy:1982:SDO,
  author =       "John L. Hennessy",
  title =        "Symbolic Debugging of Optimized Code",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "323--344",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 6 14:20:25 1996",
  bibsource =    "Compiler/bevan.bib",
  note =         "See remark \cite{Copperman:1993:TCF}.",
  abstract =     "The long-standing conflict between code optimization
                 and symbolic debugging is examined. The effects of
                 local and global optimizations on the variables of a
                 program are categorized, and models for representing
                 the effect of optimizations are given. Algorithms use
                 these models to determine the subset of variables hose
                 values do not correspond to those in the original
                 program. Restoring these variables to their correct
                 values is investigated, and empirical results from the
                 application of these algorithms to local optimization
                 are also presented.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "code generation optimization; debugging aids; directed
                 acyclic graphs; flow graphs; symbolic debugging",
  source =       "Dept. Library",
}

@Article{Sipala:1982:CSB,
  author =       "Paolo Sipala",
  title =        "Compact Storage of Binary Trees",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "345--361",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  acknowledgement = ack-pb,
}

@Article{Broy:1982:CAA,
  author =       "Manfred Broy and Peter Pepper",
  title =        "Combining Algebraic and Algorithmic Reasoning: An
                 Approach to the {Schorr-Waite} Algorithm",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "362--381",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "The basic idea of the Schorr-Waite graph-marking
                 algorithm can be precisely formulated, explained, and
                 verified in a completely applicative (functional)
                 programming style. Graphs are specified algebraically
                 as objects of an abstract data type. When formulating
                 recursive programs over such types, one can combine
                 algebraic and algorithmic reasoning: An applicative
                 depth-first-search algorithm is derived from a
                 mathematical specification by applying properties of
                 reflexive, transitive closures of relations. This
                 program is then transformed in several steps into a
                 final procedural version with the help of both
                 algebraic properties of graphs and algorithmic
                 properties reflected in the recursion structure of the
                 program.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "abstract data types; algorithms; applicative
                 (functional) programming; languages; program
                 transformation; verification",
  source =       "Dept. Library",
}

@Article{Lamport:1982:BGP,
  author =       "Leslie Lamport and Robert Shostak and Marshall Pease",
  title =        "The {Byzantine} Generals Problem",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "382--401",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Oct 17 12:24:31 1998",
  bibsource =    "Theory/ProbAlgs.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib, Compiler/bevan.bib,
                 Database/dbase.bib",
  note =         "They proved that Byzantine agreement (the subject of
                 Section~\ref{sec-byzantine}) cannot be reached unless
                 fewer than one-third of the processes are faulty. This
                 result assumes that authentication, i.e., the crypting
                 of messages to make them unforgeable, is not used. With
                 unforgeable messages, they show that the problem is
                 solvable for any $n \geq t > 0$, where $n$ is the total
                 number of processes and $t$ is the number of faulty
                 processes.",
  abstract =     "Reliable computer systems must handle malfunctioning
                 components that give conflicting information to
                 different parts of the system. This situation can be
                 expressed abstractly in terms of a group of generals of
                 the Byzantine army camped with their troops around an
                 enemy city. Communicating only by messenger, the
                 generals must agree upon a common battle plan. However,
                 one or more of them may be traitors who will try and
                 confuse the others. The problem is to find an algorithm
                 to ensure that the loyal generals will reach agreement.
                 It is shown that, using only oral messages, this
                 problem is solvable if and only if more than two-thirds
                 of the generals are loyal; so a single traitor can
                 confound two loyal generals. With unforgeable written
                 messages, the problem is solvable for any number of
                 generals and possible traitors. Applications of the
                 solutions to reliable computer systems are then
                 discussed.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "fault tolerance; interactive consistency; network
                 communications; network operating systems;
                 reliability",
  source =       "Dept. Library",
}

@Article{Paige:1982:FDC,
  author =       "Robert Paige and Shaye Koenig",
  title =        "Finite Differencing of Computable Expressions",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "402--454",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "Finite differencing is a program optimization method
                 that generalizes strength reduction, and provides an
                 efficient implementation for a host of program
                 transformations including ``iterator inversion.''
                 Finite differencing is formally specified in terms of
                 more basic transformations shown to preserve program
                 semantics. Estimates of the speedup that the technique
                 yields are given. A full illustrative example of the
                 algorithm is given.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "algorithms; automatic programming; computations on
                 discrete structures; differentiable expression;
                 languages; optimization; program transformation; SETL;
                 theory; verification; very high-level languages",
  source =       "Dept. Library",
}

@Article{Owicki:1982:PLP,
  author =       "Susan Owicki and Leslie Lamport",
  title =        "Proving Liveness Properties of Concurrent Programs",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "455--495",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Ai/nonmono.bib, Compiler/TOPLAS.bib",
  abstract =     "A liveness property asserts that program execution
                 eventually reaches some desirable state. While
                 termination has been studied extensively, many other
                 liveness properties are important for concurrent
                 programs. A formal proof method, based on temporal
                 logic, for deriving liveness properties is presented.
                 It allows a rigorous formulation of simple informal
                 arguments. How to reason with temporal logic and how to
                 use safety (invariance) properties in proving liveness
                 is shown. The method is illustrated using, first, a
                 simple programming language without synchronization
                 primitives, then one with semaphores. However, it is
                 applicable to any programming language.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "concurrent programming; fairness; languages; liveness;
                 multiprocessing; program verification; proof of
                 correctness; semantics of programming languages;
                 synchronization; temporal logic; theory; verification",
  source =       "Dept. Library",
}

@Article{Wand:1982:DTC,
  author =       "Mitchell Wand",
  title =        "Deriving Target Code as a Representation of
                 Continuation Semantics",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "496--517",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "Reynolds' technique for deriving interpreters is
                 extended to derive compilers from continuation
                 semantics. The technique starts by eliminating
                 $\lambda$-variables from the semantic equations through
                 the introduction of special-purpose combinators. The
                 semantics of a program phrase may be represented by a
                 term built from these combinators. Then associative and
                 distributive laws are used to simplify the terms. Last,
                 a machine is built to interpret the simplified terms as
                 the functions they represent. The combinators reappear
                 as the instructions of this machine. The technique is
                 illustrated with three examples.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "code generation; combinators; compilers;
                 continuations; denotational semantics; lambda calculus;
                 semantics",
  sjb =          "excellent paper",
  source =       "Dept. Library",
}

@Article{Krogh:1982:AAP,
  author =       "Fred T. Krogh",
  title =        "{ACM} Algorithms Policy",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "518--521",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 6 13:36:09 1996",
  bibsource =    "Misc/IMMD_IV.bib",
  acknowledgement = ack-nhfb,
}

@Article{Anonymous:1982:IA,
  author =       "Anonymous",
  title =        "Information for Authors",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "3",
  pages =        "522--525",
  month =        jul,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat Jan 06 12:58:29 1996",
  acknowledgement = ack-pb,
}

@Article{Herlihy:1982:VTM,
  author =       "Maurice P. Herlihy and Barbara Liskov",
  title =        "A Value Transmission Method for Abstract Data Types",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "527--551",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Thu May 26 15:49:48 1988",
  bibsource =    "Misc/programming.env.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib, Compiler/bevan.bib",
  abstract =     "Abstract data types have proved to be a useful
                 technique for structuring systems. In large systems it
                 is sometimes useful to have different regions of the
                 system use different representations for the abstract
                 data values. A technique is described for communicating
                 abstract values between such regions. The method was
                 developed for use in constructing distributed systems,
                 where the regions exist at different computers and the
                 values are communicated over a network. The method
                 defines a call-by-value semantics; it is also useful in
                 nondistributed systems wherever call by value is the
                 desired semantics. An important example of such a use
                 is a repository, such as a file system, for storing
                 long lived data.",
  checked =      "19940302",
  keywords =     "abstract data types; call by value; data translation;
                 design; distributed systems; input/output; languages;
                 long-term storage.; message communications; message
                 sending",
  sjb =          "For every type that is to be transmitted, need to
                 define encode $:: T \rightarrow XT$, decode $:: XT
                 \rightarrow T$, from these, the ``system'' generates
                 transmit $:: T\rightarrow T$ and transmit $:: XT
                 \rightarrow XT$, where $XT$ is the external
                 representation. As an example of how $XT$ may differ
                 from $T$, in the case of 2D coordinates, $T$ might be
                 cartesian whereas $XT$ may be a variant containing
                 either cartesian or polar. Note that it is up to the
                 user to decide what to do about sharing e.g. to
                 structured types having a pointer to a third.",
  source =       "Dept. Library",
}

@Article{Holt:1982:MIE,
  author =       "Richard C. Holt and David B. Wortman",
  title =        "A Model for Implementing {Euclid} Modules and
                 Prototypes",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "552--562",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "The PASCAL-based programming language EUCLID was
                 designed for use in implementing verifiable systems
                 software. The design of EUCLID includes many novel
                 extensions, including a module mechanism and a
                 substantial generalization of the PASCAL type
                 mechanism. This paper presents an implementation model
                 for two of these extensions: modules and parameterized
                 type definitions (prototypes).",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "abstract data types; data types and structures;
                 EUCLID; packages; run-time environments; systems
                 implementation language",
  sjb =          "Amongst other things discusses how to compile generics
                 e.g. macro vs. shared.",
  source =       "Dept. Library",
}

@Article{Griswold:1982:EEI,
  author =       "Ralph E. Griswold",
  title =        "The Evaluation of Expressions in {Icon}",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "563--584",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "Expressions in the Icon programming language may be
                 {\em conditional}, possibly producing no result, or
                 they may be {\em generators}, possibly producing a
                 sequence of results. Generators, coupled with a goal
                 directed evaluation mechanism, provide a concise method
                 for expression many complex computations. This paper
                 describes the evaluation of expressions in Icon and
                 presents an Icon program that explicates the semantics
                 of expression evaluation. This program also provides an
                 executable ``formalism'' that can be used as a tool to
                 design and test changes and additions to the
                 language.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "control structures; Icon; interpreters; semantics",
  source =       "Dept. Library",
}

@Article{Gergeron:1982:SAS,
  author =       "J. Gergeron and A. Dubuque",
  title =        "A Structured {APL} System",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "585--600",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "A structured APL system introducing several
                 interesting features is described. The APL group
                 concept has been considerably extended to yield a new
                 type of APL object called a segment. Segments
                 constitute the basic building blocks used to manage
                 memory and build up the workspace and the user's
                 library. The encapsulation capability provides a
                 unified scheme for handling variables, functions and
                 other APL objects, including files. A new structured
                 user library is proposed. The dynamic call of objects
                 during a terminal session links the user library to the
                 workspace. New types of variables are described along
                 with solutions to interesting problems based on them.",
  checked =      "19940302",
  keywords =     "APL; segmentation; software libraries; workspace",
  source =       "Dept. Library",
}

@Article{Baker:1982:OPA,
  author =       "T. P. Baker",
  title =        "A One-Pass Algorithm for Overload Resolution in
                 {Ada}",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "601--614",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "A simple method is presented for detecting ambiguities
                 and finding the correct interpretations of expressions
                 in the programming language Ada. Unlike previously
                 reported solutions to this problem, which require
                 multiple passes over a tree structure, the method
                 described here operates in one bottom-up pass, during
                 which a directed acyclic graph is produced. The
                 correctness of this approach is demonstrated by a brief
                 formal argument.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "Ada; compilers; overloading; translators",
  source =       "Dept. Library",
}

@Article{DeRemer:1982:ECL,
  author =       "Frank DeRemer and Thomas Pennello",
  title =        "Efficient Computation of {LALR}(1) Look-Ahead Sets",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "615--649",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Sat May 4 17:32:11 1996",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "Two relations that capture the essential structure of
                 the problem of computing LALR(1) look-ahead sets are
                 defined, an efficient algorithm is presented to compute
                 the sets in time linear in the size of the relations.
                 In particular, for a PASCAL grammar, the algorithm
                 performs fewer than 15 percent of the set unions
                 performed by the popular compiler-compiler YACC. When a
                 grammar is not LALR(1), the relations, represented
                 explicitly, provide for printing user-oriented error
                 messages that specifically indicate {\em how\/} the
                 look-ahead problem arose. In addition, certain loops in
                 the digraphs induced by these relations indicate that
                 the grammar is not LR($k$) for any $k$. Finally, on
                 oft-discovered and used but {\em incorrect\/}
                 look-ahead set algorithm is similarly based on two
                 other relations defined for the first time here. The
                 formal presentation of this algorithm should help
                 prevent its rediscovery.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "Backus-Naur form; compiler generators; context-free
                 grammar; grammar debugging.; LALR(1); LR(k); parsing;
                 strongly connected component; syntax; translator
                 writing systems",
  source =       "Dept. Library",
}

@Article{Dewar:1982:TDG,
  author =       "Robert B. K. Dewar and Micha Sharir and Elia
                 Weixelbaum",
  title =        "Transformational Derivation of a Garbage Collection
                 Algorithm",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "650--667",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/TOPLAS.bib, Compiler/garbage.collection.bib,
                 Compiler/Compiler.Lins.bib, Compiler/bevan.bib",
  abstract =     "Transformational programming is a relatively new
                 programming technique intended to derive complex
                 algorithms automatically. Initially, a set of
                 transformational rules is described, and an initial
                 specification of the problem to be programmed is given.
                 The specification is written in a high-level language
                 in a fairly compact form possibly ignoring efficiency.
                 A number of versions, called transformations, are
                 created by successively applying the transformational
                 rules starting with the initial specification. As an
                 example of the application of this technique to a
                 fairly complex case, a transformational derivation of a
                 variant of known efficient garbage collection and
                 compaction algorithm from an initial very high-level
                 specification is given. Currently, the techniques are
                 still being developed, and therefore the
                 transformations are derived manually. However, most of
                 the transformations done are of a technical nature and
                 could eventually be automated.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "algorithms; automatic programming; design; formal
                 differentiation; garbage collection; languages; loop
                 fusion; program transformation; strength reduction.;
                 transformational programming; very high level
                 languages; wide-spectrum languages",
  source =       "Dept. Library",
}

@Article{Boom:1982:WPL,
  author =       "H. J. Boom",
  title =        "A Weaker Precondition for Loops",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "668--677",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "In his book, {\em A Discipline of Programming},
                 Dijkstra presents the skeleton for a programming
                 language and defines its semantics axiomatically using
                 predicate transformers. His language involves only
                 bounded nondeterminism. He shows that unbounded
                 nondeterminism is incompatible with his axioms and his
                 continuity principle, and he argues that this is no
                 drawback because unboundedly nondeterministic machines
                 cannot be built. This paper considers the question of
                 unbounded nondeterminism. A new predicate transformer
                 is derived to handle this. A proof is given that the
                 new transformer corresponds to operational semantics,
                 and an informal argument is given that unbounded
                 nondeterminism can be a useful programming concept even
                 in the absence of nondeterministic machines.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "Ackermann's function; fair do loop; fair scheduling;
                 nondeterminism; predicate transformer; total
                 correctness; unbounded nondeterminism; weakest
                 precondition",
  source =       "Dept. Library",
}

@Article{Misra:1982:DGA,
  author =       "Jayadev Misra and K. M. Chandy",
  title =        "A Distributed Graph Algorithm: Knot Detection",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "678--686",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "A {\em knot\/} is a directed graph is [sic] a useful
                 concept in deadlock detection. A distributed algorithm
                 for identifying a knot in a graph using a network of
                 processes is presented. The algorithm is based on the
                 work of Dijkstra and Scholten.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "distributed algorithms; distributed applications;
                 graph algorithms; knot; message communication; network
                 operating systems; network problems; sequencing and
                 scheduling",
  source =       "Dept. Library",
}

@Article{Mallgren:1982:FSG,
  author =       "William R. Mallgren",
  title =        "Formal Specification of Graphic Data Types",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "687--710",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "Formal specification techniques and data abstractions
                 have seen little application to computer graphics. Many
                 of the objects and operations unique to graphics
                 programs can be handled conveniently by defining
                 special graphic data types. Not only do graphic data
                 types provide an attractive way to work with pictures,
                 but they also allow specification techniques for data
                 abstractions to be employed. Algebraic axioms, because
                 of their definitional nature, are especially well
                 suited to specifying the diversity of types useful in
                 graphics applications. In this paper, definitions are
                 given for some important concepts that appear in
                 graphics programs. Based on these definitions, some
                 illustrative graphic data types, called point, region,
                 geometric function, graphic transformation, and
                 tree-structured picture, are defined and specified
                 algebraically. A simple graphics language for line
                 drawings is created by embedding these new data types
                 in the language PASCAL. Using the specifications, an
                 outline of a correctness proof for a small programming
                 example is presented.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "abstract data types; algebraic approaches to
                 semantics; correctness proofs; graphic data type;
                 languages; specification techniques; verification",
  sjb =          "readable",
  source =       "Dept. Library",
}

@Article{Thatcher:1982:DTS,
  author =       "J. W. Thatcher and E. G. Wagner and J. B. Wright",
  title =        "Data Type Specification: Parameterization and the
                 Power of Specification Techniques",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "711--732",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib, Compiler/Compiler.Lins.bib,
                 Compiler/TOPLAS.bib",
  abstract =     "Our earlier work on abstract data types is extended by
                 the answers to a number of questions on the power and
                 limitations of algebraic specification techniques and
                 by a algebraic treatment of parameterized data types
                 like {\em set-of-(\ )\/} and {\em stacks-of(\ )}. The
                 ``hidden function'' problem (the need to include
                 operations in specifications which are wanted hidden
                 from the user) is investigated; the relative power of
                 conditional specifications and equational
                 specifications is investigated; and it is show that
                 parameterized specifications must contain ``side
                 conditions'' (e.g., that {\em finite-sets-of-d\/}
                 requires an equality predicate on $d$).",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "abstract data types; algebraic approaches to
                 semantics; algebraic specification; semantics; type
                 structure",
  sjb =          "Looks dated now",
  source =       "Dept. Library",
}

@Article{Williams:1982:DAF,
  author =       "John H. Williams",
  title =        "On the Development of the Algebra of Functional
                 Programs",
  journal =      j-TOPLAS,
  volume =       "4",
  number =       "4",
  pages =        "733--757",
  month =        oct,
  year =         "1982",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibsource =    "Compiler/bevan.bib",
  abstract =     "The development of the algebraic approach to reasoning
                 about functional programs that was introduced by Backus
                 in his Turing Award Lecture is furthered. Precise
                 definitions for the foundations on which the algebra is
                 based are given, and some new expansion theorems that
                 broaden the class of functions for which this approach
                 is applicable are proved. In particular, the class of
                 ``overrun-tolerant'' forms, nonlinear forms that
                 include some of the familiar divide-and-conquer program
                 schemes, are defined; an expansion theorem for such
                 forms is proved; and that theorem is used to show how
                 to derive expansions for some programs defined by
                 nonlinear forms.",
  acknowledgement = ack-pb,
  checked =      "19940302",
  keywords =     "algebraic approaches to semantics; applicative
                 (functional) programming; correctness proofs;
                 functional constructs; semantics; transformations",
  sjb =          "Looks dated now",
  source =       "Dept. Library",
}

@Article{Peterson:1982:UAC,
  author =       "Gary L. Peterson",
  title =        "An {$O(n\log{n})$} Unidirectional Algorithm for the
                 Circular Extrema Problem",
  journal =