Entry Kobayashi:1999:LPC from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Kobayashi:1999:LPC,
  author =       "Naoki Kobayashi and Benjamin C. Pierce and David N.
                 Turner",
  title =        "Linearity and the {Pi-Calculus}",
  journal =      j-TOPLAS,
  volume =       "21",
  number =       "5",
  pages =        "914--947",
  month =        sep,
  year =         "1999",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Tue Sep 26 10:12:58 MDT 2000",
  bibsource =    "http://www.acm.org/pubs/contents/journals/toplas/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org/pubs/articles/journals/toplas/1999-21-5/p914-kobayashi/p914-kobayashi.pdf;
                 http://www.acm.org/pubs/citations/journals/toplas/1999-21-5/p914-kobayashi/",
  abstract =     "The economy and flexibility of the pi-calculus make it
                 an attractive object of theoretical study and a clean
                 basis for concurrent language design and
                 implementation. However, such generality has a cost:
                 encoding higher-level features like functional
                 computation in pi-calculus throws away potentially
                 useful information. We show how a linear type system
                 can be used to recover important static information
                 about a process's behavior. In particular, we can
                 guarantee that two processes communicating over a
                 linear channel cannot interfere with other
                 communicating processes. After developing standard
                 results such as soundness of typing, we focus on
                 equivalences, adapting the standard notion of barbed
                 bisimulation to the linear setting and showing how
                 reductions on linear channels induce a useful ``partial
                 confluence'' of process behaviors. For an extended
                 example of the theory, we prove the validity of a
                 tail-call optimization for higher-order functions
                 represented as processes.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  generalterms = "Languages; Theory",
  keywords =     "concurrency; confluence; linear types; pi-calculus;
                 process calculi",
  subject =      "Software --- Programming Languages --- Formal
                 Definitions and Theory (D.3.1)",
}

Related entries