author = {Benjamin C. Pierce and Davide Sangiorgi},
  title = {Typing and Subtyping for Mobile Processes},
  booktitle = {Logic in Computer Science},
  year = {1993},
  note = {Full version in \bgroup\em Mathematical Structures in
                  Computer Science \egroup, Vol.\ 6, No.\ 5, 1996},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/pi.ps},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict}
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Concurrent Objects in a Process Calculus},
  booktitle = {Theory and Practice of Parallel Programming (TPPP),
                  Sendai, Japan (Nov.{} 1994)},
  editor = {Takayasu Ito and Akinori Yonezawa},
  year = {1995},
  month = apr,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = {907},
  pages = {187--215},
  short = {``Concurrent Objects in a Process Calculus,'' Benjamin C.
                  Pierce and David N. Turner, invited lecture at {\it Theory
                  and Practice of Parallel Programming (TPPP)}, Sendai, Japan
                  (Nov.{} 1994). Springer Lecture Notes in Computer Science
                  907, pp.~187--215},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict},
  url = {http://www.cis.upenn.edu/~bcpierce/papers/copc.ps}
  author = {Uwe Nestmann and Benjamin C. Pierce},
  title = {Decoding Choice Encodings},
  booktitle = {Proceedings of CONCUR '96},
  year = 1996,
  month = aug,
  note = {Full version in \bgroup\em Information and
                  Computation\egroup, 163(1): 1--59 (2000)},
  plclub = {Yes},
  bcp = {Yes},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/choice.ps},
  keys = {pict}
  author = {Benjamin C. Pierce},
  title = {Foundational Calculi for Programming Languages},
  booktitle = {Handbook of Computer Science and Engineering},
  chapter = {139},
  publisher = {CRC Press},
  year = {1996},
  editor = {Allen B. Tucker},
  plclub = {Yes},
  bcp = {Yes},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/crchandbook.ps},
  keys = {pict}
  author = {Benjamin Pierce and Davide Sangiorgi},
  title = {Behavioral Equivalence in the Polymorphic Pi-Calculus},
  year = 1997,
  booktitle = {Principles of Programming Languages (POPL)},
  note = {Full version in {\em Journal of the Association for
                  Computing Machinery (JACM)}, 47(3), May 2000},
  pages = {531--584},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/polybisim.ps},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict}
  author = {Benjamin C. Pierce and David N. Turner},
  title = {The {Pict} Programming Language},
  year = {2001},
  homepage = {http://www.cis.upenn.edu/~bcpierce/papers/pict/Html/Pict.html},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict},
  note = {This directory contains various papers, including a tutorial and user's manual, as well as complete compiler sources and installation instructions. (Be sure not to miss the artwork department!)}
  author = {Naoki Kobayashi and Benjamin C. Pierce and David N.
  title = {Linearity and the {Pi-Calculus}},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {21},
  number = {5},
  pages = {914--947},
  month = sep,
  year = {1999},
  coden = {ATPSDT},
  fullissn = {0164-0925},
  bibdate = {Tue Sep 26 10:12:58 MDT 2000},
  source = {TOPLAS db},
  note = {Summary in POPL 1996.},
  keys = {pict},
  full = {http://www.acm.org/pubs/articles/journals/toplas/1999-21-5/p914-kobayashi/p914-kobayashi.pdf;
  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
  plclub = {Yes},
  bcp = {Yes}
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Pict: A Programming Language Based on the Pi-Calculus},
  year = {2000},
  booktitle = {Proof, Language and Interaction: Essays in Honour of Robin
  editor = {Gordon Plotkin and Colin Stirling and Mads Tofte},
  publisher = {MIT Press},
  pages = {455--494},
  checked = {Yes},
  plclub = {Yes},
  bcp = {Yes},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/pict-design.ps},
  keys = {pict}