merged.bib
@COMMENT{{This file has been generated by bib2bib 1.80}}
@COMMENT{{Command line: bib2bib -s -r -oc plclub.keys -ob merged.bib -c bcp:"yes"|plclub:"yes" bcp.bib geoffw.bib jnf.bib weirich.bib zdancewic.bib}}
@COMMENT{{This file has been generated by bib2bib 1.80}}
@COMMENT{{Command line: bib2bib -ob bcp.bib-tmp -c 'not($key = "poplmark") and not($key = "AITR-474")' bcp.bib}}
@COMMENT{{This file has been generated by bib2bib 1.86}}
@COMMENT{{Command line: /usr/bin/bib2bib MS-CIS-03-26.bib MS-CIS-04-26.bib MS-CIS-05-04.bib MS-CIS-05-05.bib MS-CIS-05-07.bib MS-CIS-05-26.bib bgb-jfp.bib icfp2003-corrected.bib icfp2003.bib icfp2005.bib icfp2006.bib itrs2002.bib lics2005.bib phd-proposal.bib poplmark.bib senior-thesis.bib tldi2005.bib tr-717-04.bib wgp2006.bib -ob /home/geoffw/svnroot/web/dest-official/research/papers/geoffw.bib}}
@COMMENT{{This file has been generated by bib2bib 1.80}}
@COMMENT{{Command line: bib2bib -ob zdancewic.bib-tmp -c 'not($key = "ABFF+05")' zdancewic.bib}}
@PREAMBLE{{\newcommand{\SortNoop}[1]{}}}
@MISC{Pierce:gridapple,
AUTHOR = {Benjamin C. Pierce},
TITLE = {{\sc Gridapple}: an implementation of the {\sc ESRI} {\sc
Grid} system for the {Apple-II}},
YEAR = {1981},
NOTE = {Marketed by Environmental Systems Research Institute,
Redlands, CA},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{Pierce82,
AUTHOR = {B. C. Pierce},
TITLE = {A Microcomputer-Based Geographic Information System},
BOOKTITLE = {Proceedings of the Seventh West Coast Computer Faire},
MONTH = MAR,
YEAR = 1982,
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Larrabee&82,
AUTHOR = {T. Larrabee and K. McCall and C. Mitchell and B. C.
Pierce},
TITLE = {Gambit: {A} Video Game Programming Language},
HOWPUBLISHED = {Project report for Stanford CS-242 (Programming Language
Design)},
MONTH = {December},
YEAR = 1982,
NOTE = {See also: Larrabee, T. and Mitchell, C. ``Gambit: A
Prototyping Approach to Video Game Design.'' IEEE Software,
Vol. 1 No. 4, Oct. 1984.},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{Pierce84,
AUTHOR = {B. C. Pierce},
TITLE = {Gridapple: {A} Microcomputer-Based Geographic Information
System},
BOOKTITLE = {Harvard Computer Graphics Week},
MONTH = JUL,
YEAR = 1982,
NOTE = {Reprinted in Marble, D., et al, {\em Basic Readings in
Geographic Information Systems.} Williamsville, NY: SPAD
Systems, Ltd., 1984},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Pierce:arcinfo,
AUTHOR = {Benjamin C. Pierce},
TITLE = {{\sc Arc-Info} plotting and display subsystem},
YEAR = {1982},
NOTE = {Marketed by Environmental Systems Research Institute,
Redlands, CA, USA},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Pierce:artemis,
AUTHOR = {Benjamin C. Pierce},
TITLE = {{\sc Artemis}: a graphics editor for circuit diagrams},
YEAR = {1986},
NOTE = {Used internally at DEC Western Research Lab for the design
of the {\sc Titan} processor and power/packaging},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{Habermann&88,
AUTHOR = {A. N. Habermann and Charles Krueger and Benjamin Pierce
and Barbara Staudt and John Wenn},
TITLE = {Programming with Views},
INSTITUTION = {Carnegie Mellon University, Computer Science Department},
NUMBER = {CMU-CS-87-177},
MONTH = JAN,
YEAR = {1988},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{PIERCE89B,
KEY = {Pierce89b},
AUTHOR = {Benjamin Pierce},
TITLE = {A Decision Procedure for the Subtype Relation on
Intersection Types with Bounded Variables},
INSTITUTION = {School of Computer Science, Carnegie Mellon University},
TYPE = {Technical Report},
NUMBER = {CMU-CS-89-169},
MONTH = SEP,
YEAR = {1989},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{PIERCE89C,
KEY = {PIERCE89C},
AUTHOR = {Benjamin Pierce},
TITLE = {Bounded Quantification and Intersection Types},
MONTH = SEP,
YEAR = {1989},
NOTE = {Thesis proposal (unpublished)},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{PIERCE89,
KEY = {Pierce89},
AUTHOR = {Benjamin Pierce and Scott Dietzen and Spiro Michaylov},
TITLE = {Programming in Higher-order Typed Lambda-Calculi},
INSTITUTION = {Carnegie Mellon University},
TYPE = {Technical Report},
NUMBER = {CMU-CS-89-111},
MONTH = MAR,
YEAR = {1989},
PLCLUB = {Yes},
BCP = {Yes},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/leap.pdf},
ERRATA = {http://www.cis.upenn.edu/~bcpierce/papers/leap.errata},
KEYS = {typessurveys}
}
@TECHREPORT{HarperPierce90,
AUTHOR = {Robert W. Harper and Benjamin C. Pierce},
TITLE = {Extensible Records Without Subsumption},
INSTITUTION = {School of Computer Science, Carnegie Mellon University},
YEAR = {1990},
MONTH = FEB,
TYPE = {Technical Report},
NUMBER = {CMU-CS-90-102},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{Pierce90b,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Preliminary Investigation of a Calculus with Intersection
and Union Types},
YEAR = 1990,
MONTH = JUN,
NOTE = {Unpublished manuscript},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{HarperPierce91,
AUTHOR = {Robert Harper and Benjamin Pierce},
TITLE = {A Record Calculus Based on Symmetric Concatenation},
BOOKTITLE = {{ACM} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Orlando, Florida},
YEAR = 1991,
PAGES = {131--142},
MONTH = JAN,
NOTE = {Extended version available as Carnegie Mellon Technical
Report CMU-CS-90-157},
PLCLUB = {Yes},
BCP = {Yes}
}
@BOOK{PIERCE91,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Basic Category Theory for Computer Scientists},
YEAR = {1991},
PUBLISHER = {MIT Press},
FULLISBN = {0-262-66071-7},
ORDERINGINFO = {MIT PRESS 55 Hayward ST. Cambridge Mass 02142 USA
800-356-0343},
EUROPEINFO = {14 Bloomsbury Square London WC1A 2LP U.K. Facsimile:
071-404-0601},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {books}
}
@ARTICLE{ABADI91,
AUTHOR = {Mart\'{\i}n Abadi and Luca Cardelli and Benjamin Pierce
and Gordon Plotkin},
TITLE = {Dynamic Typing in a Statically Typed Language},
JOURNAL = {ACM Transactions on Programming Languages and Systems},
PUBLISHER = {ACM},
YEAR = 1991,
VOLUME = 13,
NUMBER = 2,
MONTH = APR,
PAGES = {237--268},
NOTE = {Summary in \bgroup\em {ACM} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Austin, Texas\egroup, 1989},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{ABADI91B,
AUTHOR = {Mart\'{\i}n Abadi and Benjamin Pierce and Gordon Plotkin},
TITLE = {Faithful Ideal Models for Recursive Polymorphic Types},
JOURNAL = {International Journal of Foundations of Computer Science},
VOLUME = 2,
NUMBER = 1,
MONTH = MAR,
YEAR = 1991,
PAGES = {1--21},
NOTE = {Summary in Fourth Annual Symposium on Logic in Computer
Science, June, 1989},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{Pierce91b,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Programming with Intersection Types, Union Types, and
Polymorphism},
INSTITUTION = {Carnegie Mellon University},
TYPE = {Technical Report},
NUMBER = {CMU-CS-91-106},
MONTH = FEB,
YEAR = {1991},
PLCLUB = {Yes},
BCP = {Yes}
}
@PHDTHESIS{PierceThesis,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Programming with Intersection Types and Bounded
Polymorphism},
SCHOOL = {Carnegie Mellon University},
MONTH = {December},
YEAR = {1991},
NOTE = {Available as School of Computer Science technical report
CMU-CS-91-205},
ASCII = {Benjamin C. Pierce, "Programming with Intersection Types
and Bounded Polymorphism." Ph.D. thesis, Carnegie Mellon
University, December, 1991. Available as School of Computer
Science technical report CMU-CS-91-205.},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Pierce:fmeet,
AUTHOR = {Benjamin C. Pierce},
TITLE = {{\sc Fmeet}: a polymorphic $\lambda$-calculus with
intersection types},
YEAR = {1991},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{HofmannPierce92:TR,
AUTHOR = {Martin Hofmann and Benjamin Pierce},
TITLE = {An Abstract View of Objects and Subtyping (Preliminary
Report)},
INSTITUTION = {University of Edinburgh, LFCS},
TYPE = {Technical Report},
NUMBER = {ECS-LFCS-92-226},
YEAR = {1992},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{Pierce92d,
AUTHOR = {Benjamin C. Pierce and Robert Pollack},
TITLE = {Higher-Order Subtyping},
YEAR = {1992},
MONTH = AUG,
NOTE = {Unpublished manuscript},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{Pierce:delegation,
AUTHOR = {Benjamin C. Pierce},
TITLE = {A Model of Delegation Based on Existential Types},
YEAR = {1993},
MONTH = APR,
NOTE = {Available electronically},
PLCLUB = {Yes},
BCP = {Yes},
KEYWORDS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/delegation.ps}
}
@MISC{Pierce:Kyoto-talk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {A Typed Higher-Order Programming Language Based on the
Pi-Calculus},
MONTH = JUL,
YEAR = {1993},
NOTE = {Invited lecture at {\em Workshop on Type Theory and its
Application to Computer Systems}, Kyoto University},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{PierceRemyTurner93,
AUTHOR = {Benjamin C. Pierce and Didier R\'emy and David N. Turner},
TITLE = {A Typed Higher-Order Programming Language Based on the
Pi-Calculus},
MONTH = JUL,
YEAR = {1993},
BOOKTITLE = {Workshop on Type Theory and its Application to Computer
Systems, Kyoto University},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{Pierce92g,
AUTHOR = {Benjamin C. Pierce},
TITLE = {F-Omega-Sub User's Manual, Version 1.4},
YEAR = {1993},
MONTH = FEB,
NOTE = {Available by FTP as part of the {\tt fomega}
implementation},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{Pierce:mutable,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Mutable Objects},
YEAR = {1993},
MONTH = JUN,
NOTE = {Draft report; available electronically},
PLCLUB = {Yes},
BCP = {Yes},
KEYWORDS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/mutable.ps}
}
@INPROCEEDINGS{PierceTurner92:POPL,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Object-Oriented Programming Without Recursive Types},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Charleston, South Carolina},
YEAR = {1993},
MONTH = JAN,
PAGES = {299--312},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{Pierce93c,
AUTHOR = {Benjamin Pierce},
TITLE = {Object-Oriented Programming in Typed Lambda-Calculus:
Exercises and Solutions},
YEAR = {1993},
MONTH = APR,
NOTE = {Lecture notes for 1992 Frankische OOrientierungstage,
University of Erlangen, Germany (revised version)},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{PierceTurner92b,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Statically Typed Friendly Functions via Partially Abstract
Types},
INSTITUTION = {University of Edinburgh, LFCS},
TYPE = {Technical Report},
NUMBER = {ECS-LFCS-93-256},
MONTH = APR,
YEAR = {1993},
NOTE = {Also available as INRIA-Rocquencourt Rapport de Recherche
No. 1899},
PLCLUB = {Yes},
BCP = {Yes},
KEYWORDS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/friendly.ps}
}
@MISC{Pierce:JFLA-talk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Typage des Traits Orient\'es-Objets},
MONTH = FEB,
YEAR = {1993},
NOTE = {Invited lecture at {\em Journe\'es Francophones des
Langages Applicatifs}, Annecy, France},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{PierceSangiorgi95,
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}
}
@MISC{Pierce:fomega,
AUTHOR = {Benjamin C. Pierce},
TITLE = {{\sc F-Omega-Sub}: a polymorphic $\lambda$-calculus with
higher-order subtyping and object-oriented extensions},
YEAR = {1993},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{Pierce92a,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Bounded Quantification is Undecidable},
JOURNAL = {Information and Computation},
YEAR = 1994,
VOLUME = 112,
NUMBER = 1,
PAGES = {131--165},
MONTH = JUL,
NOTE = {Also in C. A. Gunter and J. C. Mitchell, editors, {\em
Theoretical Aspects of Object-Oriented Programming:
Types, Semantics, and Language Design}, MIT Press, 1994. Summary in \bgroup \em {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Albuquerque, New Mexico\egroup},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/fsubpopl.ps}
}
@MISC{Pierce:COPC-talk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Concurrent Objects in a Process Calculus},
NOTE = {Invited lecture at {\em Theory and Practice of Parallel
Programming (TPPP)}, Sendai, Japan},
YEAR = 1994,
MONTH = NOV,
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{CastagnaPierce93,
AUTHOR = {Giuseppe Castagna and Benjamin Pierce},
TITLE = {Decidable Bounded Quantification},
BOOKTITLE = {Proceedings of the Twenty-First {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Portland, Oregon},
PUBLISHER = {ACM},
YEAR = 1994,
MONTH = JAN,
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/fsubnew.ps}
}
@INPROCEEDINGS{PierceSteffen95,
AUTHOR = {Benjamin C. Pierce and Martin Steffen},
REALAUTHOR = {Benjamin Pierce and Martin Steffen},
TITLE = {Higher-Order Subtyping},
BOOKTITLE = {IFIP Working Conference on Programming Concepts, Methods
and Calculi (PROCOMET)},
YEAR = 1994,
NOTE = {Full version in \bgroup\em Theoretical Computer
Science\egroup, vol.~176, no.~1--2, pp.\ 235--282, 1997
(corrigendum in TCS vol.~184 (1997), p.~247)},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/fomega.ps}
}
@TECHREPORT{SteffenPierce93:TR,
AUTHOR = {Martin Steffen and Benjamin Pierce},
TITLE = {Higher-Order Subtyping},
YEAR = {1994},
MONTH = JAN,
INSTITUTION = {LFCS, University of Edinburgh},
NUMBER = {ECS-LFCS-94-280},
NOTE = {Also available as {Universit\"at Erlangen-N\"urnberg
Interner Bericht IMMD7-01/94}. To appear in Theoretical
Computer Science.},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{HofmannPierce94a:TR,
AUTHOR = {Martin Hofmann and Benjamin Pierce},
TITLE = {Positive Subtyping},
YEAR = {1994},
MONTH = SEP,
INSTITUTION = {LFCS, University of Edinburgh},
NUMBER = {ECS-LFCS-94-303},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{PierceTurner92,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Simple Type-Theoretic Foundations for Object-Oriented
Programming},
NOTE = {Summary in \bgroup\em {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Charleston, South Carolina\egroup, 1993},
JOURNAL = {Journal of Functional Programming},
VOLUME = 4,
NUMBER = 2,
MONTH = APR,
PAGES = {207--247},
YEAR = {1994},
PLCLUB = {Yes},
BCP = {Yes},
PDF = {http://www.cis.upenn.edu/~bcpierce/papers/oop.pdf},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/oop.ps},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/oop-popl.ps},
KEYWORDS = {oop}
}
@ARTICLE{Pierce94a,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Woggles from {O}z: {W}riting Interactive Fiction},
NOTE = {Expanded version available electronically},
JOURNAL = {Leonardo: Journal of the International Society for the
Arts, Sciences, and Technology},
YEAR = {1994},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{HofmannPierce94,
AUTHOR = {Martin Hofmann and Benjamin Pierce},
TITLE = {A Unifying Type-Theoretic Framework for Objects},
JOURNAL = {Journal of Functional Programming},
VOLUME = {5},
NUMBER = {4},
PAGES = {593--635},
MONTH = OCT,
NOTE = {Previous versions appeared in the Symposium on Theoretical
Aspects of Computer Science, 1994, (pages 251--262) and,
under the title ``An Abstract View of Objects and Subtyping
(Preliminary Report),'' as University of Edinburgh, LFCS
technical report ECS-LFCS-92-226, 1992},
YEAR = 1995,
PLCLUB = {Yes},
BCP = {Yes},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/abstroop.ps},
KEYWORDS = {oop}
}
@INPROCEEDINGS{PierceTurner94:COPC,
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}
}
@INPROCEEDINGS{CastagnaPierce95,
AUTHOR = {Giuseppe Castagna and Benjamin Pierce},
TITLE = {Corrigendum: Decidable Bounded Quantification},
BOOKTITLE = {Proceedings of the Twenty-Second {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Portland, Oregon},
PUBLISHER = {ACM},
YEAR = 1995,
MONTH = JAN,
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/fsubnew-corrigendum.ps}
}
@ARTICLE{Abadi92,
AUTHOR = {Mart\'{\i}n Abadi and Luca Cardelli and Benjamin Pierce
and Didier R\'{e}my},
TITLE = {Dynamic Typing in Polymorphic Languages},
JOURNAL = {Journal of Functional Programming},
VOLUME = {5},
NUMBER = {1},
PAGES = {111--130},
MONTH = JAN,
NOTE = {Summary in \bgroup \em ACM SIGPLAN Workshop on ML and its
Applications\egroup, June 1992},
YEAR = 1995,
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Pierce:LinearPiTalk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Linearity and the Pi-Calculus},
NOTE = {Invited lecture at {\em Advances in Type Systems for
Computation}, Cambridge, England},
YEAR = 1995,
MONTH = AUG,
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{KobayashiPierceTurner:LinearPiTR,
AUTHOR = {Naoki Kobayashi and Benjamin C. Pierce and David N.
Turner},
TITLE = {Linearity and the Pi-Calculus},
YEAR = {1995},
NOTE = {Technical report, Department of Information Science,
University of Tokyo and Computer Laboratory, University of
Cambridge},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{HofmannPierce94a,
AUTHOR = {Martin Hofmann and Benjamin Pierce},
TITLE = {Positive Subtyping},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), San Francisco, California},
YEAR = {1995},
MONTH = JAN,
PAGES = {186--197},
NOTE = {Full version in \bgroup\em Information and
Computation\egroup, volume 126, number 1, April 1996. Also
available as University of Edinburgh technical report
ECS-LFCS-94-303, September 1994},
PLCLUB = {Yes},
BCP = {Yes},
KEYWORDS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/pos.ps}
}
@MISC{Pierce:LICSSurvey,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Types and Programming Languages: The Next Generation},
NOTE = {Invited tutorial at {\em Logic in Computer Science (LICS)}},
YEAR = 2003,
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {typessurveys},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/tng-lics2003-slides.pdf}
}
@MISC{Pierce:ModulesTutorial,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Advanced Module Systems: A Guide for the Perplexed},
NOTE = {Invited tutorial at {\em International Conference on Functional
Programming (ICFP)}},
YEAR = 2000,
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {typessurveys},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/modules-icfp.ps}
}
@MISC{Pierce:HorizonDayTalk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Using Types to Compare Objects and {ADT}s},
NOTE = {Invited lecture at {\em Horizon Day}, Indiana University},
YEAR = 1995,
MONTH = OCT,
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{BruceCardelliPierce96:old,
AUTHOR = {Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce},
TITLE = {Comparing Object Encodings},
BOOKTITLE = {Invited lecture at Third Workshop on Foundations of Object
Oriented Languages (FOOL 3)},
YEAR = 1996,
MONTH = JUL,
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{NestmannPierce96,
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}
}
@UNPUBLISHED{Pierce:EvenSimpler,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Even simpler type-theoretic foundations for {OOP}},
MONTH = MAR,
YEAR = {1996},
NOTE = {Manuscript (circulated electronically)},
PLCLUB = {Yes},
BCP = {Yes}
}
@INCOLLECTION{Pierce95a,
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}
}
@ARTICLE{CompagnoniPierce93,
AUTHOR = {Adriana B. Compagnoni and Benjamin C. Pierce},
TITLE = {Intersection Types and Multiple Inheritance},
PAGES = {469--501},
JOURNAL = {Mathematical Structures in Computer Science},
MONTH = OCT,
YEAR = 1996,
VOLUME = 6,
NUMBER = 5,
SOURCE = {http://theory.lcs.mit.edu/~dmjones/hbp/mscs/mscs.bib},
NOTE = {Preliminary version available as University of Edinburgh
technical report ECS-LFCS-93-275 and Catholic University
Nijmegen computer science technical report 93-18, Aug.
1993, under the title ``Multiple Inheritance via
Intersection Types''},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{KobayashiPierceTurner:LinearPi,
AUTHOR = {Naoki Kobayashi and Benjamin C. Pierce and David N.
Turner},
TITLE = {Linearity and the Pi-Calculus},
YEAR = {1996},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), St.~Petersburg Beach, Florida},
NOTE = {Full version in \bgroup\em ACM Transactions on Programming Languages and Systems\egroup, 21(5), pp. 914--947, September 1999},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{CompagnoniPierce93:old,
AUTHOR = {Adriana B. Compagnoni and Benjamin C. Pierce},
TITLE = {Multiple Inheritance via Intersection Types},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = 1996,
NOTE = {To appear. Preliminary version available as University of
Edinburgh technical report ECS-LFCS-93-275 and Catholic
University Nijmegen computer science technical report
93-18, Aug. 1993},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{OnBinaryMethods,
AUTHOR = {Kim B. Bruce and Luca Cardelli and Giuseppe Castagna and
{the Hopkins Objects Group (Jonathan Eifrig, Scott Smith,
Valery Trifonov)} and Gary T. Leavens and Benjamin Pierce},
TITLE = {On Binary Methods},
JOURNAL = {Theory and Practice of Object Systems},
VOLUME = 1,
NUMBER = 3,
PAGES = {221--242},
YEAR = 1996,
CHECKED = {No},
PLCLUB = {Yes},
BCP = {Yes},
KEYWORDS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/binary.ps}
}
@MISC{Pierce:FMOODSTalk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Processes, Types, and Observations},
NOTE = {Invited lecture at {\em Formal Methods on Open,
Object-Based Distributed Systems (FMOODS)}, Paris},
YEAR = 1996,
MONTH = MAR,
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{Pierce96a,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Types},
NOTE = {Lecture notes for an undergraduate course at Cambridge
University},
MONTH = FEB,
YEAR = 1996,
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{PierceSangiorgi96,
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}
}
@TECHREPORT{Pierce:BQB,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Bounded Quantification with Bottom},
YEAR = {1997},
INSTITUTION = {Computer Science Department, Indiana University},
SERIES = {CSCI},
NUMBER = {492},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/bqb.ps}
}
@INPROCEEDINGS{BruceCardelliPierce96:TACS,
AUTHOR = {Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce},
TITLE = {Comparing Object Encodings},
BOOKTITLE = {International Symposium on Theoretical Aspects of Computer Software (TACS)},
YEAR = 1997,
MONTH = SEP,
NOTE = {An earlier version was presented as an invited lecture at
the Third International Workshop on Foundations of Object
Oriented Languages (FOOL 3), July 1996; full version in \bgroup\em Information and Computation\egroup, 155(1--2):108-133, 1999},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{PierceSteffen95:old,
AUTHOR = {Benjamin Pierce and Martin Steffen},
TITLE = {Higher-Order Subtyping},
YEAR = 1997,
JOURNAL = {Theoretical Computer Science},
VOLUME = 176,
NUMBER = {1--2},
PAGES = {235--282},
NOTE = {Summary in IFIP Working Conference on Programming
Concepts, Methods and Calculi (PROCOMET), June 1994; also
University of Edinburgh technical report ECS-LFCS-94-280
and {Universit\"at Erlangen-N\"urnberg Interner Bericht
IMMD7-01/94}, January 1994.},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{Pierce92b,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Intersection Types and Bounded Polymorphism},
PAGES = {129--193},
JOURNAL = {Mathematical Structures in Computer Science},
MONTH = APR,
YEAR = 1997,
VOLUME = 7,
NUMBER = 2,
SOURCE = {http://theory.lcs.mit.edu/~dmjones/hbp/mscs/mscs.bib},
NOTE = {Summary in {\em Typed Lambda
Calculi and Applications}, March 1993, pp. 346--360},
ASCII = {Benjamin C. Pierce, "Intersection Types and Bounded
Polymorphism." Conference on Typed Lambda Calculi and
Applications, March, 1993},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Pierce:LFPTW,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Languages for Programming the Web},
MONTH = DEC,
YEAR = {1997},
NOTE = {Course materials for a graduate seminar on the theory and
practice of mobile agent programming. Available through
{\tt http://www.cis.upenn.edu/$sim$bcpierce/courses/629}.},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{PierceTurner:LTI-FSUB,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Local Type Argument Synthesis with Bounded Quantification},
YEAR = {1997},
INSTITUTION = {Computer Science Department, Indiana University},
MONTH = JAN,
SERIES = {CSCI},
NUMBER = {495},
PLCLUB = {Yes},
BCP = {Yes},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/lti-fsub.ps},
KEYS = {inference}
}
@TECHREPORT{PierceTurner:LTI-TR,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Local Type Inference},
YEAR = {1997},
INSTITUTION = {Computer Science Department, Indiana University},
SERIES = {CSCI},
NUMBER = {493},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{PierceTurner:PictDefn,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Pict Language Definition},
YEAR = {1997},
NOTE = {Available electronically},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{PierceTurner:PictLib,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Pict Libraries Manual},
YEAR = {1997},
NOTE = {Available electronically},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{PierceTurner:PictCompiler,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Pict: A Programming Language Based on the Pi-Calculus},
YEAR = {1997},
NOTE = {\URL{http://www.cis.upenn.edu/~bcpierce/papers/pict}},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{PictDistribution,
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!)}
}
@UNPUBLISHED{Pierce94b,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Programming in the Pi-Calculus: {A} Tutorial Introduction
to {P}ict},
YEAR = {1997},
NOTE = {Available electronically},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{Pierce98:ACReview,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Review of {A Theory of Objects}, by {A}badi and
{C}ardelli},
YEAR = {1997},
VOLUME = 40,
NUMBER = 5,
PAGES = {297--298},
JOURNAL = {The Computer Journal},
SOURCE = {Tom Melham},
PLCLUB = {Yes},
BCP = {Yes},
KEYWORDS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/ac-review.ps}
}
@ARTICLE{GhelliPierce95-OLD,
AUTHOR = {Giorgio Ghelli and Benjamin Pierce},
TITLE = {Bounded Existentials and Minimal Typing},
YEAR = {1998},
VOLUME = 193,
PAGES = {75--96},
JOURNAL = {Theoretical Computer Science},
PLCLUB = {Yes},
BCP = {Yes},
NOTE = {Circulated in manuscript form in 1992}
}
@MISC{GhelliPierce95,
AUTHOR = {Giorgio Ghelli and Benjamin Pierce},
TITLE = {Bounded Existentials and Minimal Typing},
YEAR = {1992},
NOTE = {Circulated in manuscript form. Full version in
{\em Theoretical Computer Science}, 193(1--2):75--96, February 1998.},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/exists.ps}
}
@TECHREPORT{BalasubramaniamPierce98-TR,
AUTHOR = {S. Balasubramaniam and Benjamin C. Pierce},
TITLE = {File Synchronization},
INSTITUTION = {Computer Science Department, Indiana University},
SERIES = {CSCI},
NUMBER = {507},
MONTH = APR,
YEAR = 1998,
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{PierceTurner:LTI,
AUTHOR = {Benjamin C. Pierce and David N. Turner},
TITLE = {Local Type Inference},
YEAR = 1998,
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), San Diego, California},
NOTE = {Full version in \bgroup\em ACM Transactions on Programming
Languages and Systems (TOPLAS)\egroup, 22(1), January 2000,
pp.~1--44},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {inference},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/lti.pdf},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/lti-popl.pdf},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf}
}
@INPROCEEDINGS{HofmannPierce:TD,
AUTHOR = {Martin Hofmann and Benjamin C. Pierce},
TITLE = {Type Destructors},
BOOKTITLE = {Informal proceedings of the Fourth International Workshop
on Foundations of Object-Oriented Languages (FOOL)},
EDITOR = {Didier R\'e{}my},
MONTH = JAN,
YEAR = {1998},
NOTE = {Full version in {\em Information and Computation}, 172(1)29--62 (2002)},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {oop},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/td.ps}
}
@MISC{Pierce:CONCUR-tutorial,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Type Systems for Concurrent Calculi},
MONTH = SEP,
YEAR = {1998},
NOTE = {Invited tutorial at {\em CONCUR}, Nice, France},
PLCLUB = {Yes},
BCP = {Yes}
}
@INCOLLECTION{BunemanPierce99,
AUTHOR = {Peter Buneman and Benjamin Pierce},
BOOKTITLE = {Internet Programming Languages},
TITLE = {Union Types for Semistructured Data},
YEAR = {1998},
MONTH = SEP,
PUBLISHER = {Springer-Verlag},
NOTE = {Proceedings of the International Database Programming
Languages Workshop. LNCS 1686},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {xduce},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/utssd.ps}
}
@INPROCEEDINGS{BalasubramaniamPierce98,
AUTHOR = {S. Balasubramaniam and Benjamin C. Pierce},
TITLE = {What is a file synchronizer?},
BOOKTITLE = {Fourth Annual ACM/IEEE International Conference on Mobile
Computing and Networking (MobiCom '98)},
MONTH = OCT,
YEAR = 1998,
NOTE = {Full version available as Indiana University CSCI
technical report \#507, April 1998},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/snc-mobicom.ps},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/snc.ps},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/snc-slides.ps},
KEYS = {unison},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Pierce:GlobalComputingFoolTalk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Global Computing: Some Questions for {FOOLs}},
SLIDES = {gc-fool-slides.ps},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {concurrencysurveys},
NOTE = {Invited talk at FOOL workshop},
YEAR = 2001
}
@MISC{Pierce:TypeSystemsForConcurrencyTalk,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Type Systems for Concurrent Calculi},
SLIDES = {concur98.ps},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {concurrencysurveys},
NOTE = {Invited tutorial at CONCUR},
YEAR = 1998
}
@MISC{Pierce:FileSyncTheoryAndPracticeSlides,
AUTHOR = {Benjamin C. Pierce},
TITLE = {File Synchronization: Theory and Practice},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/new-snc-slides.ps},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {unison},
YEAR = 2001
}
@MISC{Pierce:UnisonAFileSync-Slides,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Unison: A file synchronizer and its specification},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/snc-tacs-2001Oct.ps},
NOTE = {Invited talk at {\em Theoretical Aspects of Computer Software}
(TACS), Sendai, Japan},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {unison},
YEAR = 2001
}
@MISC{Pierce:snc,
AUTHOR = {Benjamin C. Pierce and Sundar Balasubramaniam, Trevor Jim
and Insup Lee and Insik Shin},
TITLE = {{\sc Snc}: a file synchronizer},
YEAR = {1998},
NOTE = {(Superseded by {\sc Unison}.)},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{IgarashiPierceWadler99,
AUTHOR = {Atsushi Igarashi and Benjamin Pierce and Philip Wadler},
TITLE = {Featherweight {J}ava: {A} Minimal Core Calculus for {J}ava
and {GJ}},
MONTH = OCT,
BOOKTITLE = {{ACM} {SIGPLAN} {C}onference on {O}bject {O}riented {P}rogramming:
{S}ystems, {L}anguages, and {A}pplications ({OOPSLA})},
YEAR = {1999},
NOTE = {Full version in ACM Transactions on Programming
Languages and Systems (TOPLAS), 23(3), May 2001},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {oop},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/fj-oopsla.ps},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf}
}
@INPROCEEDINGS{IgarashiPierce99,
AUTHOR = {Atsushi Igarashi and Benjamin C. Pierce},
TITLE = {Foundations for Virtual Types},
MONTH = JUN,
YEAR = 1999,
BOOKTITLE = {European Conference on Object-Oriented Programming (ECOOP), Lisbon, Portugal},
NOTE = {Also in informal proceedings of the
{\em Workshop on Foundations of Object-Oriented Languages
(FOOL)}, January 1999. Full version in {\em Information and
Computation}, 175(1): 34--49, May 2002},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/vt.ps}
}
@TECHREPORT{HosoyaPierce99,
AUTHOR = {Haruo Hosoya and Benjamin C. Pierce},
TITLE = {How Good is Local Type Inference?},
INSTITUTION = {University of Pennsylvania},
NUMBER = {MS-CIS-99-17},
MONTH = JUN,
YEAR = 1999,
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {inference},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/hgilti.ps}
}
@ARTICLE{KobayashiPierceTurner:LinearPi:TOPLAS,
AUTHOR = {Naoki Kobayashi and Benjamin C. Pierce and David N.
Turner},
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;
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.},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{SewellWojciechowskiPierce98,
AUTHOR = {Peter Sewell and Pawel Wojciechowski and Benjamin Pierce},
TITLE = {Location Independence for Mobile Agents},
BOOKTITLE = {Proceedings of {ICCL} '98},
EDITOR = {H. E. Bal and B. Belkhouche and L. Cardelli},
VOLUME = {1686},
SERIES = {lncs},
PUBLISHER = {Springer-Verlag},
MONTH = SEP,
YEAR = {1999},
NOTE = {An earlier version with title {\em Location-Independent
Communication for Mobile Agents: a Two-Level
Architecture\/} appeared as Technical Report 462, Computer
Laboratory, University of Cambridge, April 1999},
PLCLUB = {Yes},
BCP = {Yes},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/wipl.ps},
OFFICIAL = {http://link.springer.de/link/service/series/0558/bibs/1686/16860001.htm},
KEYS = {mobileagents}
}
@TECHREPORT{SewellWojciechowskiPierce98:TR,
AUTHOR = {Peter Sewell and Pawe{\l} T. Wojciechowski and Benjamin C.
Pierce},
TITLE = {Location-Independent Communication for Mobile Agents: a
Two-Level Architecture},
INSTITUTION = {Computer Laboratory, University of Cambridge},
YEAR = {1999},
NUMBER = {462},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{HarmonyRelationsPoster,
AUTHOR = {Aaron Bohannon and Jeffrey A. Vaughan and
Benjamin C. Pierce},
TITLE = {Relational Lenses: {A} language for defining
updateable views},
YEAR = {2005},
MONTH = OCT,
NOTE = {Poster presented at Greater Philadelphia DB/IR Day},
BCP = {Yes},
KEYS = {harmony},
PDF = {http://www.cis.upenn.edu/~bcpierce/papers/harmony-relations-dbir-poster.pdf}
}
@INPROCEEDINGS{BohannonPierceVaughan,
AUTHOR = {Aaron Bohannon and Jeffrey A. Vaughan and
Benjamin C. Pierce},
TITLE = {Relational Lenses: {A} Language for Updateable Views},
YEAR = {2006},
BOOKTITLE = {Principles of Database Systems (PODS)},
NOTE = {Extended version available as University of Pennsylvania
technical report MS-CIS-05-27},
BCP = {Yes},
PLCLUB = {Yes},
KEYS = {harmony},
PDF = {http://www.cis.upenn.edu/~bcpierce/papers/dblenses-pods.pdf},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/dblenses-tr.pdf}
}
@MISC{SahuguetPierceTannen2000,
AUTHOR = {Arnaud Sahuguet and Benjamin Pierce and Val Tannen},
TITLE = {Chaining, Referral, Subscription, Leasing: New Mechanisms
in Distributed Query Optimization},
MONTH = FEB,
YEAR = {2000},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{SahuguetPierceTannen2000a,
AUTHOR = {Arnaud Sahuguet and Benjamin Pierce and Val Tannen},
TITLE = {Distributed Query Optimization: Can Mobile Agents Help?},
MONTH = FEB,
YEAR = {2000},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{SewellWojciechowskiPierce98:old,
AUTHOR = {Peter Sewell and Pawel T. Wojciechowski and Benjamin C.
Pierce},
TITLE = {Location Independence for Mobile Agents},
YEAR = 2000,
NOTE = {To appear in an edited collection of papers (in Springer
LNCS) from the {\em Workshop on Internet Programming
Languages}, June 1998, Loyola University},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{Pierce:ICFP-invited,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Module Systems: A Guide for the Perplexed},
MONTH = SEP,
YEAR = {2000},
NOTE = {Invited talk at {\em ICFP}, Montreal},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{IgarashiPierce99:FJI,
AUTHOR = {Atsushi Igarashi and Benjamin C. Pierce},
TITLE = {On Inner Classes},
JOURNAL = {Information and Computation},
YEAR = 2002,
VOLUME = 177,
NUMBER = 1,
PAGES = {56--89},
MONTH = AUG,
NOTE = {A special issue with papers from the 7th International Workshop on Foundations of Object-Oriented Languages (FOOL){\rm, informal proceedings}. An earlier
version appeared in \emph \bgroup Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP)\egroup, Springer LNCS 1850, pages
129--153},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {oop},
CONF = {http://www.cis.upenn.edu/~bcpierce/fji.ps},
TR = {http://www.cis.upenn.edu/~bcpierce/fji-tr.ps}
}
@INCOLLECTION{PierceTurner:PictDesign,
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
Milner},
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}
}
@ARTICLE{GapeyevLevinPierce2000,
AUTHOR = {Vladimir Gapeyev and Michael Levin and Benjamin Pierce},
TITLE = {Recursive Subtyping Revealed},
JOURNAL = {Journal of Functional Programming},
VOLUME = 12,
NUMBER = 6,
PAGES = {511--548},
CHECKED = {Yes},
YEAR = {2003},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/rsr.ps},
NOTE = {Preliminary version in {\em International Conference on
Functional Programming (ICFP)}, 2000. Also appears as
Chapter 21 of {\em Types and Programming Languages}
by Benjamin C. Pierce (MIT Press, 2002).}
}
@INPROCEEDINGS{GapeyevLevinPierce2000:ICFP,
AUTHOR = {Vladimir Gapeyev and Michael Levin and Benjamin Pierce},
TITLE = {Recursive Subtyping Revealed},
BOOKTITLE = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP}), Montreal, Canada},
YEAR = {2000},
PLCLUB = {Yes},
BCP = {Yes},
NOTE = {To appear in {\em Journal of Functional Programming}}
}
@MISC{PierceSumii00,
AUTHOR = {Benjamin Pierce and Eijiro Sumii},
TITLE = {Relating Cryptography and Polymorphism},
MONTH = JUL,
YEAR = {2000},
PLCLUB = {Yes},
BCP = {Yes},
NOTE = {Some parts superseded by \cite{SumiiPierce01}},
KEYS = {security},
MANUSCRIPT = {http://www.cis.upenn.edu/~bcpierce/papers/infohide.ps}
}
@TECHREPORT{LevinPierce99:OLD1,
AUTHOR = {Michael Y. Levin and Benjamin C. Pierce},
TITLE = {TinkerType: {A} Language for Playing with Formal Systems},
MONTH = JUN,
YEAR = {2000},
BOOKTITLE = {Logical Frameworks and Metalanguages},
NOTE = {Invited talk (submitted for journal publication)},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{HosoyaPierce2000,
AUTHOR = {Haruo Hosoya and Benjamin C. Pierce},
TITLE = {{XDuce}: A Typed {XML} Processing Language (Preliminary
Report)},
BOOKTITLE = {International Workshop on the Web and Databases (WebDB)},
EDITOR = {Dan Suciu and Gottfried Vossen},
MONTH = MAY,
YEAR = {2000},
NOTE = {Reprinted in {\em The Web and Databases, Selected Papers},
Springer LNCS volume 1997, 2001},
KEYS = {xduce},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/xduce-prelim.ps},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{IgarashiPierceWadler01,
AUTHOR = {Atsushi Igarashi and Benjamin C. Pierce and Philip Wadler},
TITLE = {A Recipe for Raw Types},
YEAR = 2001,
BOOKTITLE = {Workshop on Foundations of Object-Oriented Languages
(FOOL)},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {oop},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/rfgj.ps}
}
@ARTICLE{BruceCardelliPierce96,
AUTHOR = {Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce},
TITLE = {Comparing Object Encodings},
JOURNAL = {Information and Computation},
YEAR = 1999,
MONTH = NOV,
VOLUME = 155,
NUMBER = {1/2},
PAGES = {108--133},
NOTE = {Special issue of papers from {\em
Theoretical Aspects of Computer Software (TACS 1997)}.
An earlier version appeared as an invited
lecture in the Third International Workshop on Foundations
of Object Oriented Languages (FOOL 3), July 1996},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {oop},
PS = {http://www.cis.upenn.edu/~bcpierce/papers/compobj.ps}
}
@UNPUBLISHED{JimPierceVouillon:UnisonSys,
AUTHOR = {Trevor Jim and Benjamin C. Pierce and J\'er\^ome Vouillon},
TITLE = {How to Build a File Synchronizer},
YEAR = {2003},
NOTE = {Manuscript},
PLCLUB = {Yes},
BCP = {Yes}
}
@ARTICLE{SumiiPierce01,
AUTHOR = {Eijiro Sumii and Benjamin C. Pierce},
TITLE = {Logical Relations for Encryption},
JOURNAL = {Journal of Computer Security},
YEAR = {2003},
VOLUME = {11},
NUMBER = {4},
PAGES = {521--554},
PLCLUB = {Yes},
BCP = {Yes},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/infohide2.ps},
KEYS = {security},
NOTE = {Extended abstract appeared in {\emph{14th IEEE Computer Security Foundations Workshop}}, pp.~256--269, 2001.}
}
@INPROCEEDINGS{HosoyaPierce2001,
AUTHOR = {Haruo Hosoya and Benjamin C. Pierce},
TITLE = {Regular Expression Pattern Matching},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), London, England},
YEAR = {2001},
PLCLUB = {Yes},
BCP = {Yes},
CHECKED = {Yes},
NOTE = {Full version in {\em Journal of
Functional Programming}, 13(6), Nov. 2003, pp. 961--1004},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/tapat.ps},
KEYS = {xduce}
}
@ARTICLE{HosoyaVouillonPierce2000,
AUTHOR = {Haruo Hosoya and J\'er\^ome Vouillon and Benjamin C.
Pierce},
TITLE = {Regular Expression Types for {XML}},
JOURNAL = {ACM Transactions on Programming Languages and Systems
(TOPLAS)},
YEAR = {2005},
MONTH = JAN,
VOLUME = 27,
NUMBER = 1,
PAGES = {46--90},
NOTE = {Preliminary version in ICFP 2000},
PLCLUB = {Yes},
BCP = {Yes},
CHECKED = {Yes},
KEYS = {xduce},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/regsub.ps},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/regsub-toplas.pdf}
}
@ARTICLE{HosoyaPierce2002,
AUTHOR = {Haruo Hosoya and Benjamin C. Pierce},
TITLE = {{XDuce}: A Statically Typed {XML} Processing Language},
JOURNAL = {ACM Transactions on Internet Technology},
YEAR = {2003},
VOLUME = 3,
NUMBER = 2,
MONTH = MAY,
PAGES = {117--148},
CHECKED = {Yes},
OFFICIAL = {http://doi.acm.org/10.1145/767193.767195},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {xduce}
}
@INPROCEEDINGS{Pierce-Sumii-01,
AUTHOR = {Eijiro Sumii and Benjamin Pierce},
TITLE = {The Cryptographic {$\lambda$}-Calculus: Syntax, Semantics,
Type System and Logical Relation (in Japanese)},
BOOKTITLE = {Informal Proceedings of JSSST Workshop on Programming and
Programming Languages (PPL2001)},
YEAR = {2001},
NOTE = {Best paper prize},
PLCLUB = {Yes},
BCP = {Yes}
}
@MISC{XtaticCompiler,
AUTHOR = {Vladimir Gapeyev and Michael Y. Levin and Benjamin C. Pierce and Alan Schmitt},
TITLE = {The {X}tatic Compiler and Runtime System},
YEAR = {2005},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {xtatic},
SOURCES = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic.tgz}
}
@PHDTHESIS{LevinThesis,
AUTHOR = {Michael Y. Levin},
TITLE = {Run, Xtatic, Run: Efficient Implementation of an Object-Oriented
Language with Regular Pattern Matching},
SCHOOL = {University of Pennsylvania},
YEAR = {2005},
BCP = {Yes},
KEYS = {xtatic},
PLCLUB = {Yes},
PDF = {http://www.cis.upenn.edu/~bcpierce/papers/levin-thesis.pdf}
}
@INPROCEEDINGS{GapeyevPierce03,
AUTHOR = {Vladimir Gapeyev and Benjamin C. Pierce},
TITLE = {Regular Object Types},
BOOKTITLE = {European Conference on Object-Oriented Programming (ECOOP), Darmstadt, Germany},
YEAR = {2003},
NOTE = {A preliminary version was presented at FOOL '03},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {xtatic},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/regobj.pdf},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/regobj-ecoop-slides.ps}
}
@ARTICLE{LevinPierce99,
AUTHOR = {Michael Y. Levin and Benjamin C. Pierce},
TITLE = {TinkerType: {A} Language for Playing with Formal Systems},
JOURNAL = {Journal of Functional Programming},
VOLUME = 13,
NUMBER = 2,
MONTH = MAR,
YEAR = {2003},
NOTE = {A preliminary version appeared as an invited
paper at the {\em Logical Frameworks and Metalanguages
Workshop (LFM)}, June 2000},
PLCLUB = {Yes},
BCP = {Yes},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/tt-jfp.pdf},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/tt-slides.ps},
SOURCES = {http://www.cis.upenn.edu/~bcpierce/papers/tt.tar.gz},
KEYS = {modular}
}
@UNPUBLISHED{PierceVouillon:UnisonSpec,
AUTHOR = {Benjamin C. Pierce and J\'er\^ome Vouillon},
TITLE = {Unison: A File Synchronizer and its Specification},
YEAR = {2001},
NOTE = {Manuscript},
PLCLUB = {Yes},
BCP = {Yes}
}
@TECHREPORT{PierceVouillon:UnisonSpecTR,
AUTHOR = {Benjamin C. Pierce and J\'er\^ome Vouillon},
TITLE = {What's in {U}nison? {A} Formal
Specification and Reference Implementation
of a File Synchronizer},
YEAR = {2004},
INSTITUTION = {Dept. of Computer and Information Science, University of Pennsylvania},
NUMBER = {MS-CIS-03-36},
PLCLUB = {Yes},
BCP = {Yes},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/unisonspec.pdf},
KEYS = {unison}
}
@BOOK{Pierce:TypeSystems,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Types and Programming Languages},
PUBLISHER = {MIT Press},
YEAR = 2002,
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {books},
HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/tapl},
ERRATA = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
}
@BOOK{ATTAPL,
EDITOR = {Benjamin C. Pierce},
TITLE = {Advanced Topics in Types and Programming Languages},
PUBLISHER = {MIT Press},
YEAR = 2005,
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {books},
HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/attapl}
}
@PROCEEDINGS{ISSS2002,
TITLE = {Software Security -- Theories and Systems},
EDITOR = {M. Okada and B. Pierce and A. Scedrov and H. Tokuda
and A. Yonezawa},
SERIES = {Lecture Notes in Computer Science},
NUMBER = {2609},
PUBLISHER = {Springer-Verlag},
OPTADDRESS = {Berlin},
YEAR = {2003},
NOTE = {Revised papers from the Mext-NSF-JSPS {\em International
Symposium on Software Security}, Tokyo, Japan,
November 8-10, 2002},
ISBN = {3-540-00708-3},
PLCLUB = {Yes},
BCP = {Yes}
}
@PROCEEDINGS{TACS2001,
TITLE = {Theoretical Aspects of
Computer Software (TACS), 4th International Symposium},
EDITOR = {Naoki Kobayashi and Benjamin C. Pierce},
SERIES = {Lecture Notes in Computer Science},
NUMBER = {2215},
PUBLISHER = {Springer-Verlag},
OPTADDRESS = {Berlin},
YEAR = {2001},
LOCATION = {Sendai, Japan, October 29-31, 2001},
ISBN = {3-540-42736-8},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{nwaysync,
BOOKTITLE = {International Symposium on Distributed Computing (DISC)},
EDITOR = {Shlomi Dolev},
AUTHOR = {Michael B. Greenwald and Sanjeev Khanna and
Keshav Kunal and Benjamin C. Pierce and Alan Schmitt},
TITLE = {Agreeing to Agree: {C}onflict Resolution for
Optimistically Replicated Data},
KEYS = {harmony},
PLCLUB = {Yes},
BCP = {Yes},
YEAR = 2006,
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/nway-disc.pdf},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/nway-tr.pdf},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/nway-disc-slides.pdf}
}
@INPROCEEDINGS{diff3,
AUTHOR = {Sanjeev Khanna and Keshav Kunal and Benjamin C. Pierce},
TITLE = {A Formal Investigation of Diff3},
YEAR = 2007,
MONTH = DEC,
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/diff3-short.pdf},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony},
BOOKTITLE = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS)},
EDITOR = {Arvind and Prasad}
}
@ARTICLE{Focal2005-long,
AUTHOR = {J. Nathan Foster and Michael B. Greenwald and Jonathan T. Moore
and Benjamin C. Pierce and Alan Schmitt},
TITLE = {Combinators for bidirectional tree transformations:
{A} linguistic approach to the view-update problem},
JOURNAL = {ACM Transactions on Programming Languages and Systems},
VOLUME = {29},
NUMBER = {3},
PAGES = {17},
MONTH = MAY,
YEAR = {2007},
PUBLISHER = {ACM Press},
ADDRESS = {New York, NY, USA},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl.pdf},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl-slides.pdf},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-toplas-final.pdf},
FULLAPPENDIX = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-toplas-electronic-appendix.pdf},
DOI = {http://portal.acm.org/citation.cfm?doid=1232420.1232424},
NOTE = {Preliminary version presented at
the {\em Workshop on Programming Language Technologies for
XML (PLAN-X)}, 2004; extended abstract presented at
{\em Principles of Programming Languages (POPL)}, 2005},
BCP = {Yes},
PLCLUB = {Yes},
KEYS = {harmony}
}
@MISC{Pierce:NEPLS2004,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Combinators for Bi-Directional Tree Transformations:
{A} Linguistic Approach to the View Update Problem},
MONTH = OCT,
YEAR = 2004,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-slides.pdf},
NOTE = {Invited talk at {\em New England Programming Languages Symposium}},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony}
}
@MISC{Pierce:LinksTalk2005,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Fancy Types for XML: Friend or Foe?},
MONTH = APR,
YEAR = 2005,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/linkstalk-200504.pdf},
NOTE = {Talk at {\em LINKS} workshop, April 2005},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {xtatic}
}
@MISC{Pierce:HarmonyTalkTGC,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Harmony: {T}he Art of Reconciliation},
MONTH = APR,
YEAR = 2005,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/harmony-tgc-talk-2005.pdf},
NOTE = {Invited talk at {\em Trusted Global Computing} conference,
April 2005},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony}
}
@MISC{Pierce:HarmonyTalk2003,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Harmony: A Synchronization Framework for Tree-Structured Data},
MONTH = SEP,
YEAR = 2003,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/harmonyslides-2003aug.pdf},
NOTE = {Slides from a talk presented in several places
(Cambridge, Edinburgh,
Philadelphia, Princeton) in Fall 2003},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony}
}
@MISC{Pierce:ETAPSTalk2006,
AUTHOR = {Benjamin C. Pierce},
TITLE = {The Weird World of Bi-Directional Programming},
MONTH = MAR,
YEAR = 2006,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-etapsslides.pdf},
NOTE = {ETAPS invited talk},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony}
}
@MISC{PierceFSTTCS07,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Adventures in Bi-Directional Programming},
MONTH = DEC,
YEAR = 2007,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/boomerang-fsttcs.pdf},
NOTE = {FSTTCS invited talk},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony}
}
@MISC{Pierce:MFPSTalk2008,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Types Considered Harmful},
MONTH = MAY,
YEAR = 2008,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf},
NOTE = {invited talk at {\em Mathematical Foundations
of Programming Semantics (MFPS)}},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony}
}
@MISC{Pierce:EPFLTalk2002,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Synchronize globally, compute locally},
MONTH = JUL,
YEAR = 2002,
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/harmonyslides-epfl.ps},
NOTE = {Keynote address at {\em Research Day on Global Computing},
EFPL, Lausanne},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {harmony}
}
@TECHREPORT{HocusFocusTR2003-old,
AUTHOR = {Michael B. Greenwald and Jonathan T. Moore and Benjamin C. Pierce
and Alan Schmitt},
TITLE = {A Language for Bi-Directional Tree Transformations},
YEAR = 2003,
TYPE = {Technical Report},
NUMBER = {MS-CIS-03-08},
INSTITUTION = { University of Pennsylvania},
PLCLUB = {Yes},
BCP = {Yes},
NOTE = {Revised April 2004}
}
@TECHREPORT{HarmonyOverview,
AUTHOR = {Benjamin C. Pierce and Alan Schmitt and Michael B. Greenwald},
TITLE = {Bringing {H}armony to Optimism:
{A} Synchronization Framework for Heterogeneous
Tree-Structured Data},
YEAR = 2003,
TYPE = {Technical Report},
NUMBER = {MS-CIS-03-42},
INSTITUTION = {University of Pennsylvania},
PLCLUB = {Yes},
BCP = {Yes},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/harmony-sync-tr.pdf},
KEYS = {harmony},
NOTE = {Superseded by MS-CIS-05-02}
}
@TECHREPORT{SYNCTR2005,
AUTHOR = {J. Nathan Foster and Michael B. Greenwald and Christian Kirkegaard
and Benjamin C. Pierce and Alan Schmitt},
TITLE = {Schema-Directed Data Synchronization},
MONTH = MAR,
YEAR = 2005,
TYPE = {Technical Report},
NUMBER = {MS-CIS-05-02},
INSTITUTION = {University of Pennsylvania},
NOTE = {Supersedes MS-CIS-03-42},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/sync-tr.pdf},
BCP = {Yes}
}
@ARTICLE{SYNC2005,
AUTHOR = {J. Nathan Foster and Michael B. Greenwald and Christian Kirkegaard
and Benjamin C. Pierce and Alan Schmitt},
TITLE = {Exploiting Schemas in Data Synchronization},
JOURNAL = {Journal of Computer and System Sciences},
VOLUME = {73},
NUMBER = {4},
PAGES = {669--689},
YEAR = 2007,
NOTE = {Extended abstract in
{\em Database Programming Languages (DBPL)} 2005},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/sync-tr.pdf},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/sync-dbpl.pdf},
SLIDES = {http://www.cis.upenn.edu/~jnfoster/papers/schema-sync-slides.pdf},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/sync-jcss.pdf},
KEYS = {harmony},
PLCLUB = {Yes},
BCP = {Yes}
}
@UNPUBLISHED{HocusFocus2003,
AUTHOR = {Michael B. Greenwald and Jonathan T. Moore
and Benjamin C. Pierce and Alan Schmitt},
TITLE = {A Language for Bi-Directional Tree Transformations},
YEAR = 2003,
INSTITUTION = {Department of Computer and Information Science, University of Pennsylvania},
NOTE = {Manuscript; available at \url{http://www.cis.upenn.edu/~bcpierce/papers/lenses.pdf}},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{SumiiPierce2004,
AUTHOR = {Eijiro Sumii and Benjamin C. Pierce},
TITLE = {A Bisimulation for Dynamic Sealing},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Venice, Italy},
YEAR = {2004},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {security},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/infohide3.pdf},
NOTE = {Full version in {\em Theoretical Computer Science} 375 (2007), 169--192}
}
@INPROCEEDINGS{SumiiPierce2005,
AUTHOR = {Eijiro Sumii and Benjamin C. Pierce},
TITLE = {A Bisimulation for Type Abstraction and Recursion},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Long Beach, California},
YEAR = {2005},
KEYS = {security},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/infohide5-popl.pdf},
FULL = {http://www.cis.upenn.edu/~bcpierce/papers/infohide5-jacm.pdf},
PLCLUB = {Yes},
BCP = {Yes},
NOTE = {Full version in {\em J. ACM}, 54 (5), 2007}
}
@INPROCEEDINGS{XtaticRuntime,
TITLE = {{XML} Goes Native: {R}un-time Representations for {Xtatic}},
AUTHOR = {Vladimir Gapeyev and Michael Y. Levin
and Benjamin C. Pierce and Alan Schmitt},
YEAR = 2005,
MONTH = APR,
BOOKTITLE = {14th International Conference on Compiler Construction},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-runtime-CC.pdf},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-runtime-TR.pdf},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {xtatic}
}
@INPROCEEDINGS{XTProgr,
TITLE = {Statically Typed Document Transformation: {A}n {Xtatic} Experience},
AUTHOR = {Vladimir Gapeyev and Fran\c{c}ois Garillot and Benjamin C. Pierce},
YEAR = 2006,
MONTH = JAN,
BOOKTITLE = {Workshop on Programming Language Technologies for XML (PLAN-X), informal proceedings},
PDF = {http://www.cis.upenn.edu/~bcpierce/papers/xtprogr-planx.pdf},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/xtprogr-tr.pdf},
KEYS = {xtatic},
BCP = {Yes},
PLCLUB = {Yes},
NOTE = {Available from the Xtatic web site}
}
@INPROCEEDINGS{XtaticExperience,
TITLE = {The {Xtatic} Experience},
AUTHOR = {Vladimir Gapeyev and Michael Y. Levin
and Benjamin C. Pierce and Alan Schmitt},
BOOKTITLE = {Workshop on Programming Language Technologies for XML (PLAN-X)},
PLCLUB = {Yes},
BCP = {Yes},
MONTH = JAN,
YEAR = 2005,
NOTE = {University of Pennsylvania
Technical Report MS-CIS-04-24, Oct 2004},
KEYS = {xtatic},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-experience-TR.pdf},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-experience-slides.pdf}
}
@TECHREPORT{GapeyevPierce2004,
TITLE = {Paths into Patterns},
AUTHOR = {Vladimir Gapeyev and Benjamin C. Pierce},
YEAR = 2004,
MONTH = OCT,
TYPE = {Technical Report},
NUMBER = {MS-CIS-04-25},
INSTITUTION = {University of Pennsylvania},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {xtatic},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-pathambig-TR.pdf}
}
@INPROCEEDINGS{LevinPierce05,
TITLE = {Type-based Optimization for Regular Patterns},
AUTHOR = {Michael Y. Levin and Benjamin C. Pierce},
BOOKTITLE = {Database Programming Languages (DBPL)},
YEAR = 2005,
MONTH = AUG,
BCP = {Yes},
PLCLUB = {Yes},
KEYS = {xtatic},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/tb-TR.pdf}
}
@PROCEEDINGS{ICFP05,
TITLE = {International Conference on Functional Programming (ICFP)},
EDITOR = {Benjamin C. Pierce},
PUBLISHER = {ACM Press},
YEAR = {2005},
LOCATION = {Tallinn, Estonia, September 2005},
PLCLUB = {Yes},
BCP = {Yes}
}
@INPROCEEDINGS{Foster:FTL,
AUTHOR = {J. Nathan Foster and Benjamin C. Pierce and Alan Schmitt},
TITLE = {A Logic Your Typechecker Can Count On: {U}nordered Tree Types in Practice},
BOOKTITLE = {Workshop on Programming Language Technologies for XML (PLAN-X), informal proceedings},
YEAR = {2007},
MONTH = JAN,
BCP = {Yes},
KEYS = {harmony},
PLCLUB = {Yes},
CONF = {http://www.cis.upenn.edu/~bcpierce/papers/dtts.pdf},
SLIDES = {http://www.cis.upenn.edu/~bcpierce/papers/dtts-slides.pdf}
}
@MISC{Kennedy06,
AUTHOR = {Andrew J. Kennedy and Benjamin C. Pierce},
TITLE = {On Decidability of Nominal Subtyping with Variance},
YEAR = {2006},
MONTH = SEP,
BCP = {Yes},
KEYS = {oop,subtyping},
PLCLUB = {Yes},
NOTE = {FOOL-WOOD '07},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/variance.pdf}
}
@INPROCEEDINGS{Aydemir08,
AUTHOR = {Brian Aydemir and Arthur Chargu\'{e}raud and Benjamin C. Pierce and Randy Pollack and Stephanie Weirich},
TITLE = {Engineering formal metatheory},
YEAR = {2008},
PAGES = {3--15},
PUBLISHER = {ACM},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), San Francisco, California},
YEAR = {2008},
MONTH = JAN,
BCP = {Yes},
KEYS = {poplmark},
PLCLUB = {Yes},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf}
}
@MISC{Pierce08LambdaTA,
AUTHOR = {Benjamin C. Pierce},
TITLE = {Using a Proof Assistant to Teach Programming Language Foundations, or,
Lambda, the Ultimate {TA}},
YEAR = {2008},
MONTH = APR,
BCP = {Yes},
KEYS = {poplmark},
PLCLUB = {Yes},
NOTE = {White paper},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf}
}
@INPROCEEDINGS{Boomerang07,
AUTHOR = {Aaron Bohannon and J. Nathan Foster and Benjamin C. Pierce and Alexandre Pilkiewicz and Alan Schmitt},
TITLE = {Boomerang: Resourceful Lenses for String Data},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), San Francisco, California},
YEAR = {2008},
MONTH = JAN,
BCP = {Yes},
KEYS = {harmony},
PLCLUB = {Yes},
SHORT = {http://www.cis.upenn.edu/~bcpierce/papers/boomerang.pdf},
TR = {http://www.cis.upenn.edu/~bcpierce/papers/boomerang-tr.pdf}
}
@UNPUBLISHED{HosoyaPierceTurner98,
AUTHOR = {Haruo Hosoya and Benjamin C. Pierce and David N. Turner},
TITLE = {Datatypes and Subtyping},
NOTE = {Manuscript},
PLCLUB = {Yes},
BCP = {Yes},
KEYS = {subtyping},
YEAR = 1998,
PS = {http://www.cis.upenn.edu/~bcpierce/ds.ps}
}
@PROCEEDINGS{POPL92,
TITLE = {Proceedings of the Nineteenth ACM Symposium on Principles
of Programming Languages (Albequerque, New Mexico)},
BOOKTITLE = {Proceedings of the Nineteenth ACM Symposium on Principles
of Programming Languages (Albequerque, New Mexico)},
MONTH = JAN,
YEAR = 1992
}
@TECHREPORT{Was+Wei:UPTR-2003,
AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
TITLE = {Boxes Go Bananas: Encoding higher-order abstract syntax with
parametric polymorphism (Extended Version)},
INSTITUTION = {University of Pennsylvania},
ADDRESS = {Computer and Information Science Department, Levine Hall,
3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389},
YEAR = 2003,
NUMBER = {MS-CIS-03-26},
MONTH = SEP,
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-03-26.pdf},
PLCLUB = {yes},
ABSTRACT = {
Higher-order abstract syntax is a simple technique for implementing
languages with functional programming. Object variables and binders
are implemented by variables and binders in the host language. By
using this technique, one can avoid implementing common and tricky
routines dealing with variables, such as capture-avoiding
substitution. However, despite the advantages this technique
provides, it is not commonly used because it is difficult to write
sound elimination forms (such as folds or catamorphisms) for
higher-order abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how first-class polymorphism can be used to
guarantee the parametricity of functions embedded in higher-order
abstract syntax. With this restriction, we implement a library of
iteration operators over data-structures containing functionals. From
this implementation, we derive ``fusion laws'' that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Sch\"urmann, Despeyroux and Pfenning method of enforcing
parametricity through modal types. We do so by using this library to
give a sound and complete encoding of their calculus into System
$\mathrm{F}_{\omega}$. This encoding can serve as a starting point
for reasoning about higher-order structures in polymorphic languages.}
}
@TECHREPORT{Vyt+Was+Wei:UPTR-2004,
AUTHOR = {Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich},
TITLE = {An Open and Shut Typecase (Extended Version)},
INSTITUTION = {University of Pennsylvania},
ADDRESS = {Computer and Information Science Department, Levine Hall,
3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389},
YEAR = 2004,
NUMBER = {MS-CIS-04-26},
MONTH = NOV,
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-04-26.pdf},
PLCLUB = {yes},
ABSTRACT = {
Ad-hoc polymorphism is a compelling addition to typed programming
languages. There are two different forms of ad-hoc polymorphism. With
the nominal form, the execution of an operation is determined solely
by the name of the type argument, whereas with the structural form,
operations are defined by case analysis on the structure of types.
The two forms differ in the way that they treat user-defined types.
Operations defined by the nominal approach are considered ``open''---the
programmer can add cases for new types without modifying existing
code. The operations must be extended however with specialized code for
the new types, and it may be tedious and even difficult to add extensions
that apply to a potentially large universe of user-defined types.
Structurally defined operations apply to new types by treating them as
equal to their underlying definitions, so no new cases for new types
are necessary. However this form is considered ``closed'' to extension,
as the behaviour of the operations cannot be differentiated for the
new types. This form destroys the distinctions that user-defined types
are designed to express. Both approaches have their benefits, so it
is important to provide both capabilities in a single language that is
expressive enough to decouple the ``openness'' issue from the way that
user-defined types are treated. We present such a language that supports
both forms of ad-hoc polymorphism.
}
}
@TECHREPORT{Was+Wei:UPTR-2005,
AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
TITLE = {Generalizing Parametricity Using Information Flow (Extended Version)},
INSTITUTION = {University of Pennsylvania},
ADDRESS = {Computer and Information Science Department, Levine Hall,
3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389},
YEAR = 2005,
NUMBER = {MS-CIS-05-04},
MONTH = JUN,
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-05-04-corrected.pdf},
NOTE = {A few corrections have been made since the original technical report was published. The original technical report is available as \url{http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-05-04.pdf}},
PLCLUB = {yes},
ABSTRACT = {
Run-time type analysis allows programmers to easily and concisely define
operations based upon type structure, such as serialization, iterators,
and structural equality. However, when types can be inspected at run
time, nothing is secret. A module writer cannot use type abstraction
to hide implementation details from clients: clients can determine the
structure of these supposedly ``abstract'' data types. Furthermore,
access control mechanisms do not help isolate the implementation of
abstract datatypes from their clients. Buggy or malicious authorized
modules may leak type information to unauthorized clients, so module
implementors cannot reliably tell which parts of a program rely on their
type definitions.
Currently, module implementors rely on parametric polymorphism to provide
integrity and confidentiality guarantees about their abstract datatypes.
However, standard parametricity does not hold for languages with run-time
type analysis; this paper shows how to generalize parametricity so
that it does. The key is to augment the type system with annotations
about information-flow. Implementors can then easily see which parts
of a program depend on the chosen implementation by tracking the flow
of dynamic type information.}
}
@TECHREPORT{Was:UPTR-2005,
AUTHOR = {Geoffrey Washburn},
TITLE = {Cause and Effect: Type Systems for Effects and Dependencies},
INSTITUTION = {University of Pennsylvania},
ADDRESS = {Computer and Information Science Department, Levine Hall,
3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389},
YEAR = 2005,
NUMBER = {MS-CIS-05-05},
MONTH = JUL,
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-05-05.pdf},
PLCLUB = {yes},
ABSTRACT = {
Frameworks for formal reasoning about programs are important not only
for automated tools but also for programmers. Type systems are a
popular framework both for documenting program interfaces and for
developing static analysis tools. However, type systems commonly
used in practice today fail to capture essential aspects of program
behavior: The effects and dependencies of the programs. In this paper,
we examine a prototypical effect type system in the style of Gifford
et al. and a canonical example of a dependency type system based upon
the work of Zdancewic. Finally, we show how these two type systems
can be embedded in a more general framework, a monadic type system as
developed by Pfenning and Davies.
}
}
@TECHREPORT{Dan+Wal+Was+Wei:UPTR-2005,
AUTHOR = {Daniel S. Dantas and David Walker and Geoffrey Washburn and Stephanie Weirich},
TITLE = {Poly{AML}: A Polymorphic Aspect-oriented Functional Programming Language (Extended Version)},
INSTITUTION = {University of Pennsylvania},
ADDRESS = {Computer and Information Science Department, Levine Hall,
3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389},
YEAR = 2005,
NUMBER = {MS-CIS-05-07},
PLCLUB = {yes},
MONTH = MAY,
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-05-07.pdf},
NOTE = {Revision no 727},
ABSTRACT = {
This paper defines PolyAML, a typed functional, aspect-oriented
programming language. The main contribution of PolyAML is the
seamless integration of polymorphism, run-time type analysis and
aspect-oriented programming language features. In particular, PolyAML
allows programmers to define type-safe polymorphic advice using pointcuts
constructed from a collection of polymorphic join points. PolyAML
also comes equipped with a type inference algorithm that conservatively
extends Hindley-Milner type inference. To support first-class
polymorphic point-cut designators, a crucial feature for developing
aspect-oriented profiling or logging libraries, the algorithm blends the
conventional Hindley-Milner type inference algorithm with a simple form
of local type inference.
We give our language operational meaning via a type-directed translation
into an expressive type-safe intermediate language. Many complexities
of the source language are eliminated in this translation, leading
to a modular specification of its semantics. One of the novelties
of the intermediate language is the definition of polymorphic labels
for marking control-flow points. These labels are organized in a tree
structure such that a parent in the tree serves as a representative for
all of its children. Type safety requires that the type
of each child is less polymorphic than its parent type. Similarly,
when a set of labels is assembled as a pointcut, the type of each label
is an instance of the type of the pointcut.
}
}
@TECHREPORT{Jon+Was+Wei:UPTR-2004,
AUTHOR = {Simon {Peyton~Jones} and Geoffrey Washburn and Stephanie Weirich},
TITLE = {Wobbly types: type inference for generalised algebraic data types},
INSTITUTION = {University of Pennsylvania},
ADDRESS = {Computer and Information Science Department, Levine Hall,
3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389},
YEAR = 2004,
MONTH = JUL,
NUMBER = {MS-CIS-05-26},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-05-26.pdf},
PLCLUB = {yes},
ABSTRACT = {
Generalised algebraic data types (GADTs), sometimes known as ``guarded
recursive data types'' or ``first-class phantom types'', are a simple
but powerful generalisation of the data types of Haskell and ML.
Recent works have given compelling examples of the utility of GADTs,
although type inference is known to be difficult.
It is time to pluck the fruit. Can GADTs be added to Haskell, without
losing type inference, or requiring unacceptably heavy type annotations?
Can this be done without completely rewriting the already-complex Haskell
type-inference engine, and without complex interactions with (say)
type classes? We answer these questions in the affirmative, giving
a type system that explains just what type annotations are required,
and a prototype implementation that implements it. Our main technical
innovation is \emph{wobbly types}, which express in a declarative way
the uncertainty caused by the incremental nature of typical type-inference
algorithms.
}
}
@ARTICLE{Was+Wei:JFP-2006,
AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
TITLE = {Boxes Go Bananas: Encoding higher-order abstract syntax with
parametric polymorphism (Extended Version)},
YEAR = 2008,
JOURNAL = {Journal of Functional Programming},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/bgb-jfp.pdf},
PLCLUB = {yes},
VOLUME = 18,
DOI = {doi:10.1017/S0956796807006557},
NUMBER = 1,
MONTH = JAN,
PAGES = {87--140},
ABSTRACT = {
Higher-order abstract syntax is a simple technique for implementing
languages with functional programming. Object variables and binders
are implemented by variables and binders in the host language. By
using this technique, one can avoid implementing common and tricky
routines dealing with variables, such as capture-avoiding
substitution. However, despite the advantages this technique
provides, it is not commonly used because it is difficult to write
sound elimination forms (such as folds or catamorphisms) for
higher-order abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how first-class polymorphism can be used to
guarantee the parametricity of functions embedded in higher-order
abstract syntax. With this restriction, we implement a library of
iteration operators over data-structures containing functionals. From
this implementation, we derive ``fusion laws'' that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Sch\"urmann, Despeyroux and Pfenning method of enforcing
parametricity through modal types. We do so by using this library to
give a sound and complete encoding of their calculus into System
$\mathrm{F}_{\omega}$. This encoding can serve as a starting point
for reasoning about higher-order structures in polymorphic languages.}
}
@INPROCEEDINGS{Was+Wei:ICFP-2003a,
AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
TITLE = {Boxes Go Bananas: Encoding higher-order abstract syntax with
parametric polymorphism},
BOOKTITLE = {Proceedings of the Eighth {ACM SIGPLAN} International
Conference on Functional Programming},
YEAR = 2003,
MONTH = AUG,
ADDRESS = {Uppsala, Sweden},
ORGANIZATION = {ACM SIGPLAN},
PAGES = {249--262},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/ifcp2003-corrected.pdf},
PLCLUB = {yes},
ABSTRACT = {
Higher-order abstract syntax is a simple technique for implementing
languages with functional programming. Object variables and binders
are implemented by variables and binders in the host language. By
using this technique, one can avoid implementing common and tricky
routines dealing with variables, such as capture-avoiding
substitution. However, despite the advantages this technique
provides, it is not commonly used because it is difficult to write
sound elimination forms (such as folds or catamorphisms) for
higher-order abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how first-class polymorphism can be used to
guarantee the parametricity of functions embedded in higher-order
abstract syntax. With this restriction, we implement a library of
iteration operators over data-structures containing functionals. From
this implementation, we derive ``fusion laws'' that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Sch\"{u}rmann, Despeyroux and Pfenning method of enforcing
parametricity through modal types. We do so by using this library to
give a sound and complete encoding of their calculus into System
$\mathrm{F}_{\omega}$. This encoding can serve as a starting point
for reasoning about higher-order structures in polymorphic languages.},
NOTE = {
This version fixes a number of typographical errors found in the ICFP 2003
document; there are no signficant technical changes. Generated September 2003.}
}
@INPROCEEDINGS{Was+Wei:ICFP-2003,
AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
TITLE = {Boxes Go Bananas: Encoding higher-order abstract syntax with
parametric polymorphism},
BOOKTITLE = {Proceedings of the Eighth {ACM SIGPLAN} International
Conference on Functional Programming},
YEAR = 2003,
MONTH = AUG,
ADDRESS = {Uppsala, Sweden},
ORGANIZATION = {ACM SIGPLAN},
PAGES = {249--262},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/icfp2003.pdf},
PLCLUB = {yes},
ABSTRACT = {
Higher-order abstract syntax is a simple technique for implementing
languages with functional programming. Object variables and binders
are implemented by variables and binders in the host language. By
using this technique, one can avoid implementing common and tricky
routines dealing with variables, such as capture-avoiding
substitution. However, despite the advantages this technique
provides, it is not commonly used because it is difficult to write
sound elimination forms (such as folds or catamorphisms) for
higher-order abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how first-class polymorphism can be used to
guarantee the parametricity of functions embedded in higher-order
abstract syntax. With this restriction, we implement a library of
iteration operators over data-structures containing functionals. From
this implementation, we derive ``fusion laws'' that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Sch\"{u}rmann, Despeyroux and Pfenning method of enforcing
parametricity through modal types. We do so by using this library to
give a sound and complete encoding of their calculus into System
$\mathrm{F}_{\omega}$. This encoding can serve as a starting point
for reasoning about higher-order structures in polymorphic languages.}
}
@INPROCEEDINGS{Dan+Wal+Was+Wei:2005,
AUTHOR = {Daniel S. Dantas and David Walker and Geoffrey Washburn and Stephanie Weirich},
TITLE = {Poly{AML}: A Polymorphic Aspect-oriented Functional Programming Language},
BOOKTITLE = {Proceedings of the Tenth {ACM SIGPLAN} International
Conference on Functional Programming},
YEAR = 2005,
MONTH = SEP,
ADDRESS = {Tallinn, Estonia},
ORGANIZATION = {ACM SIGPLAN},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/icfp2005.pdf},
PLCLUB = {yes},
ABSTRACT = {
This paper defines PolyAML, a typed functional, aspect-oriented
programming language. The main contribution of PolyAML is the
seamless integration of polymorphism, run-time type analysis and
aspect-oriented programming language features. In particular, PolyAML
allows programmers to define type-safe polymorphic advice using pointcuts
constructed from a collection of polymorphic join points. PolyAML
also comes equipped with a type inference algorithm that conservatively
extends Hindley-Milner type inference. To support first-class
polymorphic point-cut designators, a crucial feature for developing
aspect-oriented profiling or logging libraries, the algorithm blends the
conventional Hindley-Milner type inference algorithm with a simple form
of local type inference.
We give our language operational meaning via a type-directed translation
into an expressive type-safe intermediate language. Many complexities
of the source language are eliminated in this translation, leading
to a modular specification of its semantics. One of the novelties
of the intermediate language is the definition of polymorphic labels
for marking control-flow points. These labels are organized in a tree
structure such that a parent in the tree serves as a representative for
all of its children. Type safety requires that the type
of each child is less polymorphic than its parent type. Similarly,
when a set of labels is assembled as a pointcut, the type of each label
is an instance of the type of the pointcut.
}
}
@INPROCEEDINGS{Was+Wei:2005,
AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
TITLE = {Generalizing Parametricity Using Information Flow},
BOOKTITLE = {The Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
YEAR = 2005,
MONTH = {June},
PAGES = {62--71},
ADDRESS = {Chicago, IL},
ORGANIZATION = {{IEEE} Computer Society},
PUBLISHER = {{IEEE} Computer Society Press},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/lics2005.pdf},
PLCLUB = {yes},
ABSTRACT = {
Run-time type analysis allows programmers to easily and concisely define
operations based upon type structure, such as serialization, iterators,
and structural equality. However, when types can be inspected at run
time, nothing is secret. A module writer cannot use type abstraction
to hide implementation details from clients: clients can determine the
structure of these supposedly ``abstract'' data types. Furthermore,
access control mechanisms do not help isolate the implementation of
abstract datatypes from their clients. Buggy or malicious authorized
modules may leak type information to unauthorized clients, so module
implementors cannot reliably tell which parts of a program rely on their
type definitions.
Currently, module implementors rely on parametric polymorphism to provide
integrity and confidentiality guarantees about their abstract datatypes.
However, standard parametricity does not hold for languages with run-time
type analysis; this paper shows how to generalize parametricity so
that it does. The key is to augment the type system with annotations
about information-flow. Implementors can then easily see which parts
of a program depend on the chosen implementation by tracking the flow
of dynamic type information.
}
}
@MISC{Was:2006,
AUTHOR = {Geoffrey Washburn},
TITLE = {Proposal for \textit{Principia Narcissus: How to Avoid Being Caught by Your Reflection}},
INSTITUTION = {University of Pennsylvania},
ADDRESS = {Computer and Information Science Department, Levine Hall,
3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389},
YEAR = 2006,
MONTH = MAY,
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/phd-proposal.pdf},
PLCLUB = {yes},
ABSTRACT = {
Reflecting on type meta-data at runtime---type-directed
programming---often provides a succinct and modular solution to many
programming problems. However, type-directed programming can violate
the data abstraction techniques used in standard software engineering
practices. I propose that type-directed programming and data abstraction
can be reconciled by the application of static information-flow techniques.
I intend to explore whether this is true by (a) developing the
meta-theory to show that these protection mechanisms can ensure the
\emph{confidentiality} and \emph{integrity} of abstract data types and
(b) developing a language, \nslang, with an information-flow type and
kind system to determine whether these techniques are compatible with
type-directed programming idioms and to assess the impact these mechanisms
have on programmers.
}
}
@INPROCEEDINGS{POPLmark:2005,
AUTHOR = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn and
J. Nathan Foster and Benjamin C. Pierce and Peter Sewell and
Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich
and Steve Zdancewic},
TITLE = {Mechanized metatheory for the masses: The POPLmark Challenge},
BOOKTITLE = {The Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005)},
YEAR = 2005,
MONTH = AUG,
ADDRESS = {Oxford, England},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/poplmark.pdf},
PLCLUB = {yes},
ABSTRACT = {
How close are we to a world where every paper on programming languages is
accompanied by an electronic appendix with machine-checked proofs?
We propose an initial set of benchmarks for measuring progress in this
area. Based on the metatheory of System F_{<:}, a typed lambda-calculus
with second-order polymorphism, subtyping, and records, these benchmarks
embody many aspects of programming languages that are challenging to
formalize: variable binding at both the term and type levels, syntactic
forms with variable numbers of components (including binders), and
proofs demanding complex induction principles.
We hope that these benchmarks will help clarify the current state of the
art, provide a basis for comparing competing technologies, and motivate
further research.
}
}
@INPROCEEDINGS{Vyt+Was+Wei:TLDI-2005,
AUTHOR = { Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich },
TITLE = { An Open and Shut Typecase },
BOOKTITLE = { The Second {ACM SIGPLAN} Workshop on Types in Language Design and Implementation },
YEAR = 2005,
MONTH = JAN,
ADDRESS = {Longbeach, California},
PAGES = {13--24},
ORGANIZATION = {ACM SIGPLAN},
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/tldi2005.pdf},
PLCLUB = {yes},
ABSTRACT = {
Two different ways of defining ad-hoc polymorphic operations commonly occur in
programming languages. With the first form polymorphic operations are defined
inductively on the structure of types while with the second form polymorphic
operations are defined for specific sets of types.
In intensional type analysis operations are defined by induction on the
structure of types. Therefore no new cases are necessary for user-defined types,
because these types are equivalent to their underlying structure.
However, intensional type analysis is ``closed'' to extension, as the behavior
of the operations cannot be differentiated for the new types, thus destroying
the distinctions that these types are designed to express.
Haskell type classes on the other hand define polymorphic operations for sets
of types. Operations defined by class instances are considered ``open''---the
programmer can add instances for new types without modifying existing code. However,
the operations must be extended with specialized code for each new type, and it
may be tedious or even impossible to add extensions that apply to a large
universe of new types.
Both approaches have their benefits, so it is important to let
programmers decide which is most appropriate for their needs. In this
paper, we define a language that supports both forms of ad-hoc
polymorphism, using the same basic constructs.
}
}
@TECHREPORT{Dan+Wal+Was+Wei:PTR-2004,
AUTHOR = {Daniel S. Dantas and David Walker and Geoffrey Washburn and Stephanie Weirich},
TITLE = {Analyzing polymorphic advice},
INSTITUTION = {Princeton University},
ADDRESS = {Department of Computer Science, Princeton University,
35 Olden Street, Princeton, NJ 08544 },
YEAR = 2004,
NUMBER = {TR-717-04},
MONTH = DEC,
PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/tr-717-04.pdf},
PLCLUB = {yes},
ABSTRACT = {
We take one of the first steps towards developing a practical,
statically-typed, functional, aspect-oriented programming language
by showing how to integrate polymorphism and type analysis with
aspect-oriented programming features. In particular, we demonstrate
how to define type-safe polymorphic advice using pointcuts that unify
a collection of polymorphic join points. We also introduce a new
mechanism for specifying context-sensitive advice that involves pattern
matching against the current stack of activation records, and meshes
well with functional programming idioms. We give our language meaning
via a type-directed translation into an expressive, but fairly simple,
type-safe intermediate language. Many complexities of the source language
are eliminated in this translation, leading to a modular specification
of its semantics. One of the novelties of the intermediate language is
the definition of polymorphic labels for marking control-flow points.
These labels are organized in a tree structure such that a parent in the
tree serves as a representative for the collection of all its children.
Type safety requires that the type of each child is a generic instance
of the type of the polymorphic parent. Similarly, when a set of labels
is assembled as a pointcut, the type of each label is an instance of
the type of the pointcut.
}
}
@INPROCEEDINGS{quotient-lenses,
AUTHOR = {J. Nathan Foster and Alexandre Pilkiewcz and Benjamin C. Pierce},
TITLE = {Quotient Lenses},
NOTE = {To appear in ICFP 2008.},
MONTH = SEP,
YEAR = 2008,
JNF = {yes},
PLCLUB = {yes},
CONF = {http://www.cis.upenn.edu/~jnfoster/papers/quotient-lenses.pdf}
}
@ARTICLE{sync-provenance,
AUTHOR = {J. Nathan Foster and Grigoris Karvounarakis},
TITLE = {Provenance and Data Synchronization},
JOURNAL = {IEEE Data Engineering Bulletin},
MONTH = DEC,
YEAR = 2007,
VOL = 30,
NUMBER = 4,
PAGES = {13--21},
NOTE = {Invited paper for special issue on provenance.},
SHORT = {http://www.cis.upenn.edu/~jnfoster/papers/debull-jnfoster-gkarvoun.pdf},
JNF = {yes},
PLCLUB = {yes}
}
@INPROCEEDINGS{xml-provenance,
AUTHOR = {J. Nathan Foster and Todd J. Green and Val Tannen},
TITLE = {Annotated {XML}: {Q}ueries and Provenance},
BOOKTITLE = {Principles of Database Systems (PODS), Vancouver, BC},
MONTH = JUN,
YEAR = 2008,
CONF = {http://www.cis.upenn.edu/~jnfoster/papers/xml-provenance.pdf},
JNF = {yes},
PLCLUB = {yes}
}
@INPROCEEDINGS{boomerang,
AUTHOR = {Aaron Bohannon and J. Nathan Foster and Benjamin C. Pierce and Alexandre Pilkiewicz and Alan Schmitt},
TITLE = {Boomerang: Resourceful Lenses for String Data},
BOOKTITLE = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), San Francisco, California},
MONTH = JAN,
YEAR = 2008,
PAGES = {407--419},
CONF = { http://www.cis.upenn.edu/~jnfoster/papers/boomerang.pdf },
SLIDES = { http://www.cis.upenn.edu/~jnfoster/papers/boomerang-slides.pdf },
TR = { http://www.cis.upenn.edu/~jnfoster/papers/boomerang-tr.pdf },
JNF = {yes},
PLCLUB = {yes}
}
@INPROCEEDINGS{pads-generic,
AUTHOR = {Mary Fernandez and Kathleen Fisher and J. Nathan Foster and Michael Greenberg and Yitzhak Mandelbaum},
TITLE = {A Generic Programming Toolkit for PADS/ML: First-Class Upgrades for Third-Party Developers},
BOOKTITLE = {Symposium on Practical Aspects of Declarative Languages (PADL), San Francisco, CA},
MONTH = JAN,
YEAR = 2008,
CONF = {http://www.cis.upenn.edu/~jnfoster/papers/pads-first-class.pdf},
PAGES = {133--149},
JNF = {yes},
PLCLUB = {yes}
}
@INPROCEEDINGS{xquery-vm,
AUTHOR = {J. Nathan Foster and Ravi Konuru and Jerome Simeon and Lionel Villard},
TITLE = {An Algebraic Approach to XQuery View Maintenance},
BOOKTITLE = { ACM {SIGPLAN} {W}orkshop on {P}rogramming {L}anguage {T}echnologies for {XML} (PLAN-X), San Francisco, CA},
MONTH = JAN,
YEAR = 2008,
PAGES = 31,
SHORT = {http://www.cis.upenn.edu/~jnfoster/papers/xquery-maintenance.pdf},
SLIDES = {http://www.cis.upenn.edu/~jnfoster/papers/xquery-maintenance-slides.pdf},
JNF = {yes},
PLCLUB = {yes}
}
@INCOLLECTION{FJ-afp,
AUTHOR = {J. Nathan Foster and Dimitrios Vytiniotis},
TITLE = {A Theory of Featherweight Java in Isabelle/HOL},
BOOKTITLE = {The Archive of Formal Proofs},
EDITOR = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
PUBLISHER = {\url{http://afp.sf.net}},
MONTH = APR,
YEAR = 2006,
SHORT = {http://www.cis.upenn.edu/~jnfoster/papers/FJ-outline.pdf},
FULL = {http://www.cis.upenn.edu/~jnfoster/papers/FJ-document.pdf},
SOURCES = {http://www.cis.upenn.edu/~jnfoster/papers/FJ.tar.gz},
JNF = {Yes},
PLCLUB = {yes}
}
@INPROCEEDINGS{looj04,
AUTHOR = {Kim B. Bruce and J. Nathan Foster},
TITLE = {{LOOJ}: Weaving {LOOM} into {J}ava},
BOOKTITLE = {European Conference on Object-Oriented Programming (ECOOP), Oslo, Norway},
PAGES = {389-413},
YEAR = {2004},
MONTH = JUN,
VOLUME = {3086},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
CONF = { http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3086&spage=389 },
SLIDES = {http://www.cis.upenn.edu/~jnfoster/papers/looj-slides.pdf},
PLCLUB = {yes},
JNF = {yes}
}
@INPROCEEDINGS{vytiniotis:fph,
AUTHOR = {Dimitrios Vytiniotis and Stephanie Weirich and Simon Peyton Jones},
TITLE = {FPH: First-class polymorphism for Haskell},
BOOKTITLE = {ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming },
YEAR = 2008,
ADDRESS = {Victoria, BC, Canada},
MONTH = SEP,
PLCLUB = {Yes},
PDF = {http://www.seas.upenn.edu/~sweirich/papers/icfp08.pdf},
PROJECTURL = {http://www.cis.upenn.edu/~dimitriv/fph},
ABSTRACT = {Languages supporting polymorphism typically have ad-hoc restrictions
on where polymorphic types may occur. Supporting ``first-class'' polymorphism,
by lifting those restrictions, is obviously desirable, but it is hard
to achieve this without sacrificing type inference. We present a new
type system for higher-rank and impredicative polymorphism that improves
on earlier proposals: it is an extension of Damas-Milner;
it relies only on System F types; it has a simple, declarative specification;
it is robust to program transformations; and it enjoys a complete and decidable
type inference algorithm.
}
}
@INPROCEEDINGS{vytiniotis07a,
AUTHOR = {Dimitrios Vytiniotis and Stephanie Weirich},
TITLE = {Dependent types: Easy as {PIE}},
BOOKTITLE = {Draft Proceedings of the 8th Symposium on Trends in Functional Programming},
PAGES = {XVII-1---XVII-15},
YEAR = 2007,
EDITOR = {Marco T. Moraz\'{a}n and Henrik Nilsson},
MONTH = APR,
ORGANIZATION = {Dept. of Math and Computer Science, Seton Hall University},
NOTE = {TR-SHU-CS-2007-04-1},
PDF = {http://www.seas.upenn.edu/~sweirich/papers/tfp07.pdf},
PLCLUB = {yes}
}
@INPROCEEDINGS{vytiniotis:parametricity,
AUTHOR = {Dimitrios Vytiniotis and Stephanie Weirich},
TITLE = {Free theorems and runtime type representations},
BOOKTITLE = {Mathematical Foundations of Programming Semantics (MFPS XXIII)},
MONTH = APR,
YEAR = 2007,
PAGES = {357--373},
ADDRESS = {New Orleans, LA, USA},
PLCLUB = {yes},
PDF = {http://www.seas.upenn.edu/~sweirich/papers/rtheorems07.pdf},
PS = {http://www.seas.upenn.edu/~sweirich/papers/rtheorems07.ps},
PROJECTURL = {http://www.cis.upenn.edu/~dimitriv/parametricity/},
ABSTRACT = {
Reynolds' abstraction theorem, often referred to
as the parametricity theorem, can be used to derive properties about
functional programs solely from their types. Unfortunately, in the
presence of runtime type analysis, the abstraction properties of
polymorphic programs are no longer valid. However, runtime type
analysis can be implemented with term-level representations of
types, as in the language of Crary et
al., where case analysis on
these runtime representations introduces type refinement. In this
paper, we show that representation-based analysis is consistent with
type abstraction by extending the abstraction theorem to such a
language. We also discuss the ``free theorems'' that result. This
work provides a foundation for the more general problem of extending
the abstraction theorem to languages with generalized algebraic
datatypes.
}
}
@INPROCEEDINGS{aydemir+:nominal-coq,
AUTHOR = {Brian Aydemir and Aaron Bohannon and Stephanie Weirich},
TITLE = {Nominal Reasoning Techniques in {Coq}},
BOOKTITLE = {International Workshop on Logical Frameworks and
Meta-Languages:Theory and Practice (LFMTP) },
YEAR = 2006,
ADDRESS = {Seattle, WA, USA},
MONTH = AUG,
PDF = {http://www.seas.upenn.edu/~sweirich/papers/nominal-coq/lfmtp06.pdf},
PROJECTURL = {http://www.seas.upenn.edu/~sweirich/papers/nominal-coq/},
PLCLUB = {yes},
PAGES = { 60--69},
ABSTRACT = {
We explore an axiomatized nominal approach to variable binding in Coq,
using an untyped lambda-calculus as our test case. In our nominal
approach, alpha-equality of lambda terms coincides with Coq's built-in
equality. Our axiomatization includes a nominal induction principle and
functions for calculating free variables and substitution. These axioms
are collected in a module signature and proved sound
using locally nameless terms as the underlying
representation. Our experiences so far suggests that it is feasible to
work from such axiomatized theories in Coq and that the nominal style of
variable binding corresponds closely with paper proofs. We are currently
working on proving the soundness of a primitive recursion combinator
and developing a method of generating these axioms and their proof of
soundness from a grammar describing the syntax of terms and binding.
}
}
@INPROCEEDINGS{weirich:replib,
AUTHOR = {Stephanie Weirich},
TITLE = {{RepLib}: {A} library for derivable type classes},
BOOKTITLE = {Haskell Workshop},
MONTH = SEP,
ADDRESS = {Portland, OR, USA},
YEAR = 2006,
PLCLUB = {yes},
PAGES = {1--12},
PDF = {http://repository.upenn.edu/cis_papers/362},
PROJECTURL = {http://www.seas.upenn.edu/~sweirich/RepLib/},
ABSTRACT = {
Some type class instances can be automatically derived from the
structure of types. As a result, the Haskell language includes the
"deriving" mechanism to automatic generates such instances for a
small number of built-in type classes. In this paper, we present
RepLib, a GHC library that enables a similar mechanism for arbitrary
type classes. Users of RepLib can define the relationship between
the structure of a datatype and the associated instance declaration
by a normal Haskell functions that pattern-matches a representation
types. Furthermore, operations defined in this manner are
extensible---instances for specific types not defined by type
structure may also be incorporated. Finally, this library also
supports the definition of operations defined by parameterized
types.
}
}
@INPROCEEDINGS{washburn:good-advice,
AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
TITLE = {Good Advice for Type-directed Programming:
{A}spect-oriented Programming and Extensible Generic Functions},
MONTH = SEP,
PLCLUB = {yes},
YEAR = 2006,
PDF = {http://www.seas.upenn.edu/~sweirich/papers/aspect-tdp.pdf},
PROJECTURL = {http://www.cs.princeton.edu/sip/projects/aspectml/},
BOOKTITLE = {Workshop on Generic Programming (WGP)},
ADDRESS = {Portland, OR, USA},
PAGES = {33--44},
ABSTRACT = {
Type-directed programming is an important idiom for software design.
In type-directed programming the behavior of programs is guided by the
type structure of data. It makes it possible to implement many sorts
of operations, such as serialization, traversals, and queries, only
once and without needing to continually revise their implementation as
new data types are defined.
Type-directed programming is the basis for recent research into
"scrapping" tedious boilerplate code that arises in functional
programming with algebraic data types. This research has primarily
focused on writing type-directed functions that are closed to
extension. However, L\"ammel and Peyton Jones recently developed a
technique for writing openly extensible type-directed functions in
Haskell by making clever use of type classes. Unfortunately, this
technique has a number of limitations.
We present an alternate approach to writing openly extensible
type-directed functions by using the aspect-oriented programming
features provided by the language AspectML. Our solution not only
avoids the limitations present in L\"ammel and Peyton Jones technique,
but also allows type-directed functions to be extended at any time
with cases for types that were not even known at compile-time. This
capability is critical to writing programs that make use of dynamic
loading or runtime type generativity.
}
}
@INPROCEEDINGS{vytiniotis+:boxy,
TOPIC = {language design},
HISTORICAL = {The paper shows how type inference can exploit user annotations in order to type check programs
that require first-class polymorphism. This revision of th