merged.bib
@comment{{This file has been generated by bib2bib 1.97}}
@comment{{Command line: bib2bib -s -r -oc plclub.keys -ob merged.bib -c bcp:"yes"|plclub:"yes" bcp.bib weirich.bib zdancewic.bib}}
@comment{{This file has been generated by bib2bib 1.97}}
@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.97}}
@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},
keys = {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},
keys = {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},
keys = {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},
keys = {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},
keys = {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},
keys = {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:ICMTtalk,
author = {Benjamin C. Pierce},
title = {Foundations for Bidirectional Programming, or: {H}ow To Build
a Bidirectional Programming Language},
note = {Keynote address at {\em International Conference
on Model Transformation (ICMT)}},
year = 2009,
month = jun,
plclub = {Yes},
bcp = {Yes},
keys = {harmony},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/icmt-2009-slides.pdf}
}
@misc{Pierce:LambdaTA,
author = {Benjamin C. Pierce},
title = {Lambda, The Ultimate {TA}: {U}sing a Proof Assistant to Teach
Programming Language Foundations},
note = {Keynote address at {\em International Conference on
Functional Programming (ICFP)}},
year = 2009,
plclub = {Yes},
month = sep,
bcp = {Yes},
keys = {poplmark},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA.pdf}
}
@misc{Pierce:LambdaTA-ITP,
author = {Benjamin C. Pierce},
title = {Proof Assistant
as Teaching Assistant: A View from the Trenches},
note = {Keynote address at {\em International Conference
on Interactive Theorem Proving (ITP)}},
year = 2010,
plclub = {Yes},
month = jul,
bcp = {Yes},
keys = {poplmark},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-ITP.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{EncyOfDBs09,
author = {V\'{e}ronique Benzaken and Giuseppe Castagna and Haruo
Hosoya and Benjamin C. Pierce and Stijn Vansummeren},
title = {{XML} Typechecking},
booktitle = {Encyclopedia of Database Systems},
publisher = {Springer},
year = {2009},
plclub = {Yes},
bcp = {Yes},
keys = {xduce}
}
@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},
keys = {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},
keys = {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} (Sumii and Pierce, 2001)},
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 = {unison},
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 = {unison},
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 = {unison}
}
@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 = {unison}
}
@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 = {typessurveys,contracts}
}
@misc{Pierce:Onward2010,
author = {Benjamin C. Pierce},
title = {creativity: sensitivity and surprise},
month = oct,
year = 2010,
slides = {http://www.cis.upenn.edu/~bcpierce/cgi-bin/photos/Onward.pdf},
note = {Keynote talk at {\em SPLASH / Onward!}},
plclub = {Yes},
bcp = {Yes},
keys = {misc}
}
@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 = {unison}
}
@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 = {unison},
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},
keys = {unison}
}
@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}
}
@proceedings{POPL09,
title = {Principles of Programming Languages (POPL)},
editor = {Benjamin C. Pierce},
publisher = {ACM Press},
year = {2009},
location = {Savannah, Georgia, January 2009},
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},
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}
}
@inproceedings{Greenberg10,
author = {Michael Greenberg and Benjamin C. Pierce and Stephanie Weirich},
title = {Contracts Made Manifest},
year = {2010},
publisher = {ACM},
booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Madrid, Spain},
month = jan,
bcp = {Yes},
keys = {contracts},
plclub = {Yes},
short = {http://www.cis.upenn.edu/~bcpierce/papers/contracts-popl.pdf}
}
@misc{Pierce08LambdaTA,
author = {Benjamin C. Pierce},
title = {Using a Proof Assistant to Teach Programming Language Foundations, or,
{L}ambda, 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{QuotientLenses08,
author = {J. Nathan Foster and Alexandre Pilkiewicz and Benjamin
C. Pierce},
title = {Quotient Lenses},
booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP}), Victoria, Canada},
year = {2008},
month = sep,
bcp = {Yes},
keys = {harmony},
plclub = {Yes},
short = {http://www.cis.upenn.edu/~bcpierce/papers/quotient-lenses.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}
}
@inproceedings{updatable-security-views,
author = {J. Nathan Foster and Benjamin C. Pierce and Steve Zdancewic},
title = {Updatable Security Views},
booktitle = {IEEE Computer Security Foundations Symposium (CSF), Port Jefferson, NY},
month = jul,
year = 2009,
bcp = {yes},
plclub = {yes},
conf = {http://www.cis.upenn.edu/~jnfoster/papers/updatable-security-views.pdf}
}
@misc{Pierce:POPL09ChairsReport,
author = {Benjamin C. Pierce},
title = {POPL 2009 PC Chair's Report},
month = jan,
year = {2009},
plclub = {Yes},
bcp = {Yes},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/popl09-chairs-reports.pdf}
}
@book{Pierce:SF,
author = {Benjamin C. Pierce and Chris Casinghino and
Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu and Vilhelm Sjoberg and Brent Yorgey},
title = {Software Foundations},
year = {2012},
publisher = {Electronic textbook},
plclub = {Yes},
bcp = {Yes},
keys = {poplmark,books},
note = {\URL{http://www.cis.upenn.edu/~bcpierce/sf}},
ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
japanese = {http://proofcafe.org/sf}
}
@misc{Spiders,
author = {Benjamin C. Pierce and Alessandro Romanel and Daniel Wagner},
title = {The {Spider Calculus}: Computing in Active Graphs},
year = {2010},
plclub = {Yes},
bcp = {Yes},
keys = {mobileagents},
manuscript = {http://www.cis.upenn.edu/~bcpierce/papers/spider_calculus.pdf}
}
@inproceedings{DPCS2010,
author = {Jason Reed and Adam J. Aviv and Daniel
Wagner and Andreas Haeberlen and Benjamin C. Pierce and
Jonathan M. Smith},
title = {Differential Privacy for Collaborative Security},
booktitle = {European Workshop on System Security (EUROSEC)},
year = {2010},
month = apr,
plclub = {Yes},
bcp = {Yes},
keys = {security},
manuscript = {http://www.cis.upenn.edu/~bcpierce/papers/eurosec2010.pdf}
}
@inproceedings{HofmannPierceWagner10,
author = {Martin Hofmann and Benjamin C. Pierce and Daniel Wagner},
title = {Symmetric Lenses},
year = {2011},
booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Austin, Texas},
month = jan,
bcp = {yes},
plclub = {yes},
keys = {harmony},
short = {http://www.cis.upenn.edu/~bcpierce/papers/symmetric.pdf},
full = {http://www.cis.upenn.edu/~bcpierce/papers/symmetric-full.pdf}
}
@inproceedings{HofmannPierceWagner12,
author = {Martin Hofmann and Benjamin C. Pierce and Daniel Wagner},
title = {Edit Lenses},
year = {2012},
booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), Philadelphia, Pennsylvania},
month = jan,
bcp = {yes},
plclub = {yes},
keys = {harmony},
short = {http://dmwit.com/papers/201107EL.pdf},
slides = {http://dmwit.com/papers/201107EL_slides.pdf}
}
@inproceedings{Matching10,
author = {Davi M. J. Barbosa and Julien Cretin and Nate Foster
and Michael Greenberg and Benjamin C. Pierce},
title = {Matching Lenses: Alignment and View Update},
year = {2010},
month = sep,
booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP}), Baltimore, Maryland},
bcp = {yes},
plclub = {yes},
keys = {harmony},
tr = {http://repository.upenn.edu/cis_reports/915/},
short = {http://www.cis.upenn.edu/~bcpierce/papers/alignment.pdf}
}
@inproceedings{ReedPierce10,
author = {Jason Reed and Benjamin C. Pierce},
title = {Distance Makes the Types Grow Stronger:
{A} Calculus for Differential Privacy},
booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP}), Baltimore, Maryland},
year = {2010},
month = sep,
bcp = {yes},
plclub = {yes},
keys = {security},
short = {http://www.cis.upenn.edu/~bcpierce/papers/dp.pdf},
long = {http://privacy.cis.upenn.edu/papers/metric-pres-tr.pdf}
}
@inproceedings{BohannonPierce10,
author = {Aaron Bohannon and Benjamin C. Pierce},
title = {Featherweight {F}irefox:
{F}ormalizing the Core of a Web Browser},
booktitle = {Usenix Conference on Web Application Development (WebApps)},
year = {2010},
month = jun,
bcp = {yes},
plclub = {yes},
keys = {security},
short = {http://www.cis.upenn.edu/~bcpierce/papers/webapps_2010_bohannon_final.pdf}
}
@inproceedings{Bohannon&09,
author = {Bohannon, Aaron and Pierce, Benjamin C. and Sj\"{o}berg, Vilhelm and Weirich, Stephanie and Zdancewic, Steve},
title = {Reactive Noninterference},
booktitle = {CCS '09: Proceedings of the 16th ACM conference on Computer and communications security},
year = {2009},
isbn = {978-1-60558-894-0},
pages = {79--90},
location = {Chicago, Illinois, USA},
doi = {http://doi.acm.org/10.1145/1653662.1653673},
publisher = {ACM},
address = {New York, NY, USA},
bcp = {yes},
plclub = {yes},
keys = {security}
}
@inproceedings{Haeberlen&11,
author = {Andreas Haeberlen and Benjamin C. Pierce and
Arjun Narayan},
title = {Differential Privacy Under Fire},
booktitle = {Proceedings of the 20th USENIX Security Symposium},
location = {San Francisco, CA},
month = aug,
year = {2011},
bcp = {yes},
plclub = {yes},
keys = {security},
pdf = {http://www.cis.upenn.edu/~ahae/papers/fuzz-sec2011.pdf}
}
@inproceedings{DBLP:conf/esop/BeloGIP11,
author = {Jo{\~a}o Filipe Belo and
Michael Greenberg and
Atsushi Igarashi and
Benjamin C. Pierce},
title = {Polymorphic Contracts},
booktitle = {European Symposium on Programming (ESOP), Saarbr{\"u}cken, Germany},
year = {2011},
pages = {18-37},
ee = {http://dx.doi.org/10.1007/978-3-642-19718-5_2},
bcp = {Yes},
plclub = {Yes},
keys = {contracts},
crossref = {DBLP:conf/esop/2011},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/esop/2011,
editor = {Gilles Barthe},
title = {Programming Languages and Systems - 20th European Symposium
on Programming, ESOP 2011, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2011,
Saarbr{\"u}cken, Germany, March 26-April 3, 2011.
Proceedings},
booktitle = {ESOP},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6602},
year = {2011},
isbn = {978-3-642-19717-8},
ee = {http://dx.doi.org/10.1007/978-3-642-19718-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{SAFEPLOS11,
author = {
Andr\'{e} DeHon and
Ben Karel and
Thomas F. Knight Jr. and
Gregory Malecha and
Beno\^{i}t Montagu and
Robin Morisset and
Greg Morrisett and
Benjamin C. Pierce and
Randy Pollack and
Sumit Ray and
Olin Shivers and
Jonathan M. Smith and
Gregory Sullivan
},
title = {Preliminary Design of the SAFE Platform},
month = oct,
year = 2011,
bcp = {Yes},
plclub = {Yes},
keys = {security},
pdf = {http://www.crash-safe.org/sites/default/files/plos11-submission.pdf},
booktitle = {Proceedings of the 6th Workshop on Programming
Languages and Operating Systems (PLOS 2011)},
location = {Cascais, Portugal}
}
@misc{Pierce:PLMW-talk,
author = {Benjamin C. Pierce},
title = {Types},
month = jan,
year = 2012,
slides = {http://www.cis.upenn.edu/~bcpierce/papers/PLMW-2012.pdf},
note = {Invited talk at {\em Programming Languages
Mentoring Workshop}},
keys = {typessurveys},
plclub = {Yes},
bcp = {Yes}
}
@misc{CRASH-PLPV-2012.pdf,
author = {Benjamin C. Pierce},
title = {Verification Challenges of Pervasive Information Flow},
month = jan,
year = 2012,
slides = {http://www.cis.upenn.edu/~bcpierce/papers/CRASH-PLPV-2012.pdf},
note = {Invited talk at {\em Programming Languages
Meets Program Verification} workshop (PLPV)},
plclub = {Yes},
bcp = {Yes},
keys = {security}
}
@misc{TypesALaMilner,
author = {Benjamin C. Pierce},
title = {Types {\` a} la {M}ilner},
month = apr,
year = 2012,
slides = {http://www.cis.upenn.edu/~bcpierce/papers/TypesALaMilner.pdf},
note = {Invited talk at {\em Milner Symposium}},
keys = {typessurveys},
plclub = {Yes},
bcp = {Yes}
}
@misc{TypesALaMilner-ETE,
author = {Benjamin C. Pierce},
title = {Types {\` a} la {M}ilner},
month = apr,
year = 2012,
video = {http://youtu.be/carP8i6YSZs},
note = {Talk at {\em Philly Emerging Technologies Conference}},
keys = {typessurveys},
plclub = {Yes},
bcp = {Yes}
}
@misc{Pierce-PODS12,
author = {Benjamin C. Pierce},
title = {Linguistic Foundations for Bidirectional Transformations},
month = may,
year = 2012,
note = {Invited tutorial at {\em Principles of Database Systems (PODS)}},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/PODStutorial2012.pdf},
keys = {harmony},
plclub = {Yes},
bcp = {Yes}
}
@misc{GenLabels,
title = {A Theory of Information-Flow Labels},
author = {Beno\^it Montagu and
Benjamin C. Pierce and
Randy Pollack and
Adrien Sur\'ee},
month = jul,
year = {2012},
howpublished = {Draft},
bcp = {Yes},
keys = {security},
manuscript = {http://www.cis.upenn.edu/~bcpierce/papers/toifl-prelim.pdf}
}
@misc{NaVs,
title = {Exceptionally Available Dynamic IFC},
author = {C\u{a}t\u{a}lin Hri\c{t}cu and
Michael Greenberg and
Ben Karel and
Benjamin C. Pierce and
Greg Morrisett},
month = jul,
year = {2012},
howpublished = {Draft},
bcp = {Yes},
keys = {security},
manuscript = {http://www.cis.upenn.edu/~bcpierce/papers/navs-prelim.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}
}
@misc{weirich:flops12,
author = {Stephanie Weirich},
title = {Dependently typed programming in GHC},
note = {Invited talk given at FLOPS 2012},
slides = {http://www.seas.upenn.edu/~sweirich/talks/flops2012.pdf},
month = {May},
year = 2012,
plclub = {Yes}
}
@misc{weirich:tlca11,
author = {Stephanie Weirich},
title = {Combining Proofs and Programs},
note = {Joint invited speaker for Rewriting Techniques and Applications (RTA 2011) and Typed Lambda Calculi and Applications (TLCA 2011)},
slides = {http://www.seas.upenn.edu/~sweirich/talks/tlca-2011.pdf},
month = jun,
year = 2011,
plclub = {Yes}
}
@inproceedings{ccasin:msfp12,
author = {Chris Casinghino and Vilhelm Sj\"{o}berg and Stephanie Weirich},
title = {Step-Indexed Normalization for a Language with General Recursion},
booktitle = {Fourth workshop on Mathematically Structured Functional Programming (MSFP '12)},
year = 2012,
pdf = {papers/msfp12log.pdf},
plclub = {yes}
}
@inproceedings{sjoberg:msfp12,
author = {Vilhelm Sj\"oberg and Chris Casinghino and Ki Yung Ahn and
Nathan Collins and Harley D. Eades III and Peng Fu
and Garrin Kimmell and Tim Sheard and Aaron Stump
and Stephanie Weirich},
title = {Irrelevance, Heterogenous Equality, and Call-by-value Dependent Type Systems},
booktitle = {Fourth workshop on Mathematically Structured Functional Programming (MSFP '12)},
year = 2012,
plclub = {yes},
pdf = {papers/msfp12prog.pdf}
}
@inproceedings{kimmel:plpv,
author = {Garrin Kimmell and Aaron Stump and Harley D. Eades III and
Peng Fu and Tim Sheard and Stephanie Weirich and Chris Casinghino
and Vilhelm Sj\"oberg and Nathan Collins and Ki Yung Ahn},
title = {Equational Reasoning about Programs with General Recursion and Call-by-value Semantics},
booktitle = {Sixth ACM SIGPLAN Workshop Programming Languages meets Program Verification (PLPV '12)},
year = 2012,
plclub = {Yes},
pdf = {papers/plpv2012genreccbv.pdf}
}
@inproceedings{weirich:lifting,
author = {Brent A. Yorgey and Stephanie Weirich and
Julien Cretin and Simon {Peyton Jones} and
Dimitrios Vytiniotis and Jos\'{e} Pedro Magalha\~{e}s},
title = {Giving Haskell A Promotion},
booktitle = {Seventh ACM SIGPLAN Workshop on. Types in Language Design and Implementation (TLDI '12)},
year = 2012,
pdf = {http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf},
plclub = {Yes}
}
@inproceedings{weirich:binders,
author = {Stephanie Weirich and Brent A. Yorgey and Tim Sheard},
title = {Binders Unbound},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/icfp11.pdf},
booktitle = {Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming},
series = {ICFP '11},
year = {2011},
isbn = {978-1-4503-0865-6},
location = {Tokyo, Japan},
pages = {333--345},
numpages = {13},
url = {http://doi.acm.org/10.1145/2034773.2034818},
acmid = {2034818},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {generic programming, haskell, name binding, patterns},
plclub = {Yes}
}
@inproceedings{stump:position,
author = {Tim Sheard and Aaron Stump and Stephanie Weirich},
title = {Language-Based Verification Will Change The World},
booktitle = {2010 FSE/SDP Workshop on the Future of Software Engineering Research},
year = 2010,
month = nov,
plclub = {yes},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/foser10.pdf},
note = {Position paper.}
}
@inproceedings{weirich:newtypes,
author = {Stephanie Weirich and Dimitrios Vytiniotis and Simon {Peyton Jones}
and Steve Zdancewic},
title = {Generative Type Abstraction and Type-level Computation},
booktitle = {POPL 11: 38th {ACM SIGACT-SIGPLAN} Symposium on Principles of Programming Languages, January 26--28, 2011. Austin, TX, USA.},
year = 2011,
publisher = {ACM},
month = jan,
plclub = {yes},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf},
abstract = {Modular languages support generative type abstraction,
ensuring that an abstract type is distinct from its
representation, except inside the implementation where the
two are synonymous. We show that this well-established
feature is in tension with the non-parametric features
of newer type systems, such as indexed type families and GADTs.
In this paper we solve the problem by using kinds to
distinguish between parametric and non-parametric contexts.
The result is directly applicable to Haskell, which is rapidly
developing support for type-level computation, but the same
issues should arise whenever generativity and non-parametric features
are combined.}
}
@proceedings{Haskell09,
title = {Haskell Symposium},
editor = {Stephanie Weirich},
publisher = {ACM Press},
year = {2009},
month = aug,
location = {Edinburgh, Scotland, August 2009},
plclub = {Yes}
}
@misc{Weirich:Haskell09ChairsReport,
author = {Stephanie Weirich},
title = {Haskell 2009 PC Chair's Report},
month = aug,
year = {2009},
plclub = {Yes}
}
@proceedings{ICFP10,
title = {International Conference on Functional Programming},
editor = {Stephanie Weirich},
publisher = {ACM Press},
year = {2010},
month = sep,
location = {Baltimore, MD, September 2010},
plclub = {Yes}
}
@misc{Weirich:ICFP10ChairsReport,
author = {Stephanie Weirich},
title = {ICFP 2010 PC Chair's Report},
month = sep,
year = {2010},
plclub = {Yes}
}
@inproceedings{teqt,
author = {Aaron Stump and Vilhelm Sj\"{o}berg and Stephanie Weirich},
title = {Termination Casts: A Flexible Approach to Termination with
General Recursion},
booktitle = {Workshop on Partiality and Recursion in Interactive Theorem Provers},
year = 2010,
address = {Edinburgh, Scotland},
plclub = {yes},
month = jul,
pdf = {http://www.seas.upenn.edu/~sweirich/papers/submitted-PAR-10-Proceedings.pdf},
abstract = {
This paper proposes a type-and-effect system called $\ensuremath{\texttt{T}^{\texttt{eq}\downarrow}}$, which
distinguishes terminating terms and total functions from possibly
diverging terms and partial functions, for a lambda calculus with
general recursion and equality types. The central idea is to include
a primitive type-form ``Terminates t'', expressing that term t is
terminating; and then allow terms t to be coerced from possibly
diverging to total, using a proof of Terminates t. We call such
coercions \emph{termination casts}, and show how to implement
terminating recursion using them. For the meta-theory of the system,
we describe a translation from $\ensuremath{\texttt{T}^{\texttt{eq}\downarrow}}$ to a logical theory of
termination for general recursive, simply typed functions. Every
typing judgment of $\ensuremath{\texttt{T}^{\texttt{eq}\downarrow}}$ is translated to a theorem expressing the
appropriate termination property of the computational part of the
$\ensuremath{\texttt{T}^{\texttt{eq}\downarrow}}$ term.
}
}
@inproceedings{iseq,
author = {Limin Jia and Jianzhou Zhao and Vilhem Sj\"{o}berg and Stephanie Weirich},
title = {Dependent types and Program Equivalence},
booktitle = {37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
year = 2010,
address = {Madrid, Spain},
month = jan,
organization = {ACM},
plclub = {yes},
pages = {275--286},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/popl10-lambda-eek.pdf},
project = {http://www.cis.upenn.edu/~plclub/lambda-eek},
abstract = {The definition of type equivalence is one of the most important design
issues for any typed language. In dependently-typed languages, because
terms appear in types, this definition must rely on a definition of
term equivalence. In that case, decidability of type checking requires
decidability for the term equivalence relation.
Almost all dependently-typed languages require this relation to be
decidable. Some, such as Coq, Epigram or Agda, do so by employing
analyses to force all programs to terminate. Conversely, others, such
as DML, ATS, Omega, or Haskell, allow nonterminating computation, but
do not allow those terms to appear in types. Instead, they identify a
terminating index language and use singleton types to connect indices
to computation. In both cases, decidable type checking comes at a
cost, in terms of complexity and expressiveness.
Conversely, the benefits to be gained by decidable type checking are
modest. Termination analyses allow dependently typed programs to
verify total correctness properties. However, decidable type checking
is not a prerequisite for type safety. Furthermore, decidability does
not imply tractability. A decidable approximation of program
equivalence may not be useful in practice.
Therefore, we take a different approach: instead of a fixed notion for
term equi valence, we parameterize our type system with an abstract
relation that is not n ecessarily decidable. We then design a novel
set of typing rules that require on ly weak properties of this
abstract relation in the proof of the preservation an d progress
lemmas. This design provides flexibility: we compare valid instantiat
ions of term equivalence which range from beta-equivalence, to
contextual equiva lence, to some exotic equivalences.
}
}
@article{vytiniotis:romega,
author = {Dimitrios Vytiniotis and Stephanie Weirich},
title = {Parametricity, Type Equality and Higher-order Polymorphism},
journal = {Journal of Functional Programming},
year = 2010,
month = mar,
volume = 20,
number = 2,
pages = {175--210},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~sweirich/papers/gparam-jfp2.pdf},
abstract = {
Propositions that express type equality are a frequent ingredient of
modern functional programming---they can encode generic
functions, dynamic types, and GADTs. Via the Curry-Howard
correspondence, these propositions are ordinary types
inhabited by proof terms, computed using runtime type
representations. In this paper we show that two examples of type
equality propositions actually do reflect type equality; they are
only inhabited when their arguments are equal and their proofs are
unique (up to contextual equivalence.) We show this result in the
context of a strongly normalizing language with higher-order
polymorphism and primitive recursion over runtime type
representations by proving Reynolds's abstraction theorem. We then
use this theorem to derive ``free'' theorems about equality types.
}
}
@incollection{weirich:aritygen-journal,
author = {Stephanie Weirich and Chris Casignhino},
editor = {Jeremy Gibbons},
booktitle = {Generic and Indexed Programming},
title = {Generic Programming with Dependent Types},
publisher = {Springer-Verlag Berlin Heidelberg},
year = 2012,
pdf = {http://www.cis.upenn.edu/~sweirich/papers/ssgip-journal.pdf},
number = 7470,
series = {Lecture Notes in Computer Science},
plclub = {yes},
pages = {217--258}
}
@inproceedings{aritygen,
author = {Stephanie Weirich and Chris Casinghino},
title = {Arity-generic type-generic programming},
booktitle = {{ACM SIGPLAN} Workshop on Programming Languages Meets Program Verification (PLPV)},
pages = {15--26},
month = jan,
plclub = {yes},
year = 2010,
pdf = {http://www.seas.upenn.edu/~sweirich/papers/aritygen.pdf}
}
@techreport{aydemir:lngen,
title = {LNgen: Tool Support for Locally Nameless Representations},
author = {Brian Aydemir and Stephanie Weirich},
institution = {Computer and Information Science, University of Pennsylvania},
month = jun,
year = 2010,
plclub = {yes},
number = {MS-CIS-10-24},
pdf = {http://repository.upenn.edu/cis_reports/933},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/MS-CIS-10-24.pdf},
projecturl = {http://www.cis.upenn.edu/~sweirich/papers/lngen/}
}
@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},
pages = {295--306},
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 the boxy types paper offers a new smart-application rule,
that outperforms the versions of smart-application appearing in earlier drafts.
Many parts have been rewritten and clarified.},
title = {Boxy type inference for higher-rank types and impredicativity},
booktitle = {International Conference on Functional Programming (ICFP)},
abstract = {
Languages with rich type systems are beginning to
employ a blend of type inference and type
checking, so that the type inference engine is
guided by programmer-supplied type annotations. In
this paper we show, for the first time, how to combine
the virtues of two well-established ideas:
unification-based inference, and bidirectional
propagation of type annotations. The result is a type
system that conservatively extends Hindley-Milner, and
yet supports both higher-rank types and
impredicativity. },
author = {Dimitrios Vytiniotis and Stephanie Weirich and Simon L. {Peyton Jones}},
month = sep,
year = 2006,
pdf = {http://repository.upenn.edu/cis_papers/275/},
projecturl = {http://www.cis.upenn.edu/%7Edimitriv/dimitriv-inference.html},
category = {fcp},
address = {Portland, OR, USA},
plclub = {yes},
pages = { 251--262}
}
@inproceedings{pj-vytiniotis:wobbly,
author = {Simon L. {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
title = {Simple unification-based type inference for {GADTs}},
booktitle = {International Conference on Functional Programming (ICFP)},
historical = {This paper differs from previous versions of the ``wobbly types'' paper in that the ambiguity caused
by unification is now recorded in the environments and typing judgements instead of the types. The most
recent addition is the notion of the ``fresh most general unifier'', which eliminates problems arising from
the directionality of arbitrary most general unifiers, when they are used for GADT type refinement.},
abstract = {
Generalized algebraic data types (GADTs), sometimes known as ``guarded
recursive data types'' or ``first-class phantom
types'', are a simple but powerful generalization 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. Our
contribution is to show how to exploit
programmer-supplied type annotations to make the type
inference task almost embarrassingly easy. Our main
technical innovation is wobbly types, which express in
a declarative way the uncertainty caused by the
incremental nature of typical type-inference
algorithms. },
month = sep,
year = 2006,
plclub = {yes},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/gadt.pdf},
category = {gadt},
projecturl = {http://www.cis.upenn.edu/%7Edimitriv/dimitriv-inference.html},
address = {Portland, OR, USA},
pages = {50--61}
}
@techreport{vytiniotis+:gadt-techreport,
topic = {language design},
author = {Dimitrios Vytiniotis and Stephanie Weirich and Simon L. {Peyton~Jones}},
title = {Simple unification-based type inference for {GADTs}, {Technical Appendix}},
institution = {University of Pennsylvania},
year = 2006,
number = {MS-CIS-05-22},
month = {April},
category = {gadt},
cattype = {report},
plclub = {Yes},
projecturl = {http://www.cis.upenn.edu/%7Edimitriv/dimitriv-inference.html},
pdf = {http://www.cis.upenn.edu/~dimitriv/wobbly/wobbly-techreport.pdf}
}
@article{peyton-jones+:practical,
author = {Simon L. {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Mark Shields},
title = {Practical type inference for arbitrary-rank types},
journal = {Journal of Functional Programming},
year = 2007,
plclub = {yes},
pages = {1--82},
volume = 17,
number = 1,
month = jan,
projecturl = {http://www.cis.upenn.edu/%7Edimitriv/dimitriv-inference.html},
pdf = {http://repository.upenn.edu/cis_papers/315/},
abstract = {
Haskell's popularity has driven the need for ever more expressive type
system features, most of which threaten the decidability and
practicality of Damas-Milner type inference. One such feature is the
ability to write functions with higher-rank types --- that is,
functions that take polymorphic functions as their arguments.
Complete type inference is known to be undecidable for higher-rank
(impredicative) type systems, but in practice programmers are more
than willing to add type annotations to guide the type inference
engine, and to document their code. However, the choice of just what
annotations are required, and what changes are required in the type
system and its inference algorithm, has been an ongoing topic of
research.
We take as our starting point a lambda-calculus proposed by Odersky
and Laufer. Their system supports arbitrary-rank polymorphism through
the exploitation of type annotations on lambda-bound arguments and
arbitrary sub-terms. Though elegant, and more convenient than some
other proposals, Odersky and Laufer's system requires many
annotations. We show how to use local type inference (invented by
Pierce and Turner) to greatly reduce the annotation burden, to the
point where higher-rank types become eminently usable.
Higher-rank types have a very modest impact on type inference. We
substantiate this claim in a very concrete way, by presenting a
complete type-inference engine, written in Haskell, for a traditional
Damas-Milner type system, and then showing how to extend it for
higher-rank types. We write the type-inference engine using a monadic
framework: it turns out to be a particularly compelling example of
monads in action.
The paper is long, but is strongly tutorial in style.
}
}
@inproceedings{weirich+:tdj,
plclub = {yes},
author = {Stephanie Weirich and Liang Huang},
title = {A Design for Type-Directed {Java}},
booktitle = {Workshop on Object-Oriented Developments (WOOD)},
year = 2004,
editor = {Viviana Bono},
series = {ENTCS},
pages = {117-136},
annote = {An extended version of this paper is
University of Pennsylvania
Computer and Information Science Technical Report
MS-CIS-04-11.},
projecturl = {http://www.seas.upenn.edu/%7Esweirich/tdj/tdj.htm},
pdf = {http://repository.upenn.edu/cis_papers/275/},
ps = {http://www.cis.upenn.edu/~lhuang3/pubs/tdj-short.ps},
abstract = {
Type-directed programming is an important and widely used
paradigm in the design of software. With this form of programming,
an application may analyze type information to determine its
behavior. By analyzing the structure of data, many operations, such
as serialization, cloning, adaptors and iterators may be defined
once, for all types of data. That way, as the program evolves, these
operations need not be updated---they will automatically adapt to
new data forms. Otherwise, each of these operations must be
individually redefined for each type of data, forcing programmers to
revisit the same program logic many times during a program's
lifetime.
The Java language supports type directed programming with the
instanceof operator and the Java Reflection API. These
mechanisms allow Java programs to depend on the name and structure
of the run-time classes of objects. However, the Java mechanisms
for type-directed programming are difficult to use. They also do not
integrate well with generics, an important new feature of the Java
language.
In this paper, we describe the design of several expressive new
mechanisms for type-directed programming in Java, and show that
these mechanisms are sound when included in a language similar to
Featherweight Java. Basically, these new mechanisms pattern-match
the name and structure of the type parameters of generic code,
instead of the run-time classes of objects. Therefore, they
naturally integrate with generics and provide strong guarantees
about program correctness. As these mechanisms are based on pattern
matching, they naturally and succinctly express many operations that
depend on type information. Finally, they provide programmers with
some degree of protection for their abstractions. Whereas
instanceof and reflection can determine the exact run-time type
of an object, our mechanisms allow any supertype to be supplied for
analysis, hiding its precise structure.}
}
@article{weirich:cast-journal,
plclub = {yes},
author = {Stephanie Weirich},
title = {Type-Safe Cast},
journal = {Journal of Functional Programming},
month = nov,
year = 2004,
volume = 14,
number = 6,
pages = {681-695},
pdf = {http://journals.cambridge.org/bin/bladerunner?REQUNIQ=1098990699&REQSESS=1422511&118000REQEVENT=&REQINT1=254715&REQAUTH=0},
abstract = { Comparing two types for equality is an essential ingredient for an
implementation of dynamic types. Once equality has been established,
it is safe to cast a value from one type to another. In a language
with run-time type analysis, implementing such a procedure is fairly
straightforward. Unfortunately, this naive implementation destructs
and rebuilds the argument while iterating over its type structure.
However, by using higher-order polymorphism, a casting function can
treat its argument parametrically. We demonstrate this solution in
two frameworks for ad-hoc polymorphism: intensional type analysis
and Haskell type classes.}
}
@article{weirich:erasure,
author = {Stephanie Weirich},
title = {Type-Safe Run-time Polytypic Programming},
journal = {Journal of Functional Programming},
year = 2006,
month = nov,
pages = {681--710},
plclub = {yes},
volume = 16,
number = 10,
pdf = {http://www.seas.upenn.edu/~sweirich/papers/erasure/erasure-jfp.pdf},
abstract = {
Polytypic programming is a way of defining type-indexed
operations, such as map, fold and zip, based on type information.
Run-time polytypic programming allows that type information to
be dynamically computed---this support is essential in modern
programming languages that support separate compilation, first-class
type abstraction, or polymorphic recursion.
However, in previous work we defined run-time polytypic programming
with a type-passing semantics. Although it is natural to define
polytypic programs as operating over first-class types, such a
semantics suffers from a number of drawbacks. This paper describes
how to recast that work in a type-erasure semantics, where terms
represent type information in a safe manner. The resulting language
is simple and easy to implement---we present a prototype
implementation of the necessary machinery as a small Haskell
library.
}
}
@techreport{huang+:tdp-tr,
plclub = {yes},
author = {Liang Huang and Stephanie Weirich},
title = {A Design for Type-Directed Programming in {Java}
(Extended Version)},
institution = {University of Pennsylvania, Computer and Information Science},
year = 2004,
number = {MS-CIS-04-11},
month = oct,
pages = {1--49},
ps = {http://www.seas.upenn.edu/~sweirich/papers/tdj/ms-cis-04-11.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/tdj/ms-cis-04-11.pdf}
}
@phdthesis{weirich:phd,
plclub = {yes},
author = {Stephanie Weirich},
title = {Programming With Types},
school = {Cornell University},
month = aug,
year = 2002,
ps = {http://www.seas.upenn.edu/~sweirich/papers/thesis/thesis.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/thesis/thesis.pdf},
abstract = {Run-time type analysis is an increasingly important linguistic
mechanism in modern programming languages. Language runtime
systems use it to implement services such as accurate garbage
collection, serialization, cloning and structural
equality. Component frameworks rely on it to provide reflection
mechanisms so they may discover and interact with program
interfaces dynamically. Run-time type analysis is also crucial
for large, distributed systems that must be dynamically extended,
because it allows those systems to check program invariants when
new code and new forms of data are added. Finally, many generic
user-level algorithms for iteration, pattern matching, and
unification can be defined through type analysis mechanisms.
However, existing frameworks for run-time type analysis were
designed for simple type systems. They do not scale well to the
sophisticated type systems of modern and next-generation
programming languages that include complex constructs such as
first-class abstract types, recursive types, objects, and type
parameterization. In addition, facilities to support type
analysis often require complicated language semantics that allow
little freedom in their implementation. This dissertation
investigates the foundations of run-time type analysis in the
context of statically-typed, polymorphic programming languages.
Its goal is to show how such a language may support
type-analyzing operations in a way that balances expressiveness,
safety and simplicity.}
}
@inproceedings{weirich:hota,
plclub = {yes},
author = {Stephanie Weirich},
title = {Higher-Order Intensional Type Analysis},
booktitle = {11th European Symposium on Programming (ESOP)},
editor = {Daniel Le M\'{e}tayer},
pages = {98--114},
year = 2002,
month = apr,
address = {Grenoble, France},
ps = {http://www.seas.upenn.edu/~sweirich/papers/hota/hota.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/hota/hota.pdf},
abstract = {Intensional type analysis provides the ability to
analyze abstracted types at run time. In this paper, we extend
that ability to higher-order and kind-polymorphic type
constructors. The resulting language is elegant and expressive:
we show through examples how it extends the repertoire of
polytypic functions that may be defined.}
}
@inproceedings{weirich01,
plclub = {yes},
author = {Stephanie Weirich},
title = {Encoding Intensional Type Analysis},
booktitle = {10th European Symposium on Programming (ESOP)},
year = 2001,
editor = {D. Sands},
pages = {92--106},
address = {Genova, Italy},
month = apr,
annote = {2001 Springer-Verlag. Minor corrections in local version.},
url = {http://link.springer.de/link/service/series/0558/tocs/t2028.htm},
ps = {http://www.seas.upenn.edu/~sweirich/papers/depabs/depabs.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/depabs/depabs.pdf},
abstract = {Languages for intensional type analysis permit ad-hoc
polymorphism, or run-time analysis of types. However, such
languages require complex, specialized constructs to support this
operation, which hinder optimization and complicate the
meta-theory of these languages. In this paper, we observe that
such specialized operators need not be intrinsic to the language,
and in fact, their operation may be simulated through standard
encodings of iteration in the polymorphic lambda
calculus. Therefore, we may more easily add intensional analysis
operators to complicated languages via a translation semantics,
instead of through language extension.}
}
@inproceedings{weirich00,
plclub = {yes},
author = {Stephanie Weirich},
title = {Type-Safe Cast: Functional Pearl},
booktitle = {Proceedings of theFifth {ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP})},
year = 2000,
month = sep,
address = {Montreal, Canada},
pages = {58--67},
abstract = {In a language with non-parametric or ad-hoc
polymorphism, it is possible to determine the identity of a type
variable at run time. With this facility, we can write a function
to convert a term from one abstract type to another, if the two
hidden types are identical. However, the naive implementation of
this function requires that the term be destructed and rebuilt. In
this paper, we show how to eliminate this overhead using
higher-order type abstraction. We demonstrate this solution in two
frameworks for ad-hoc polymorphism: intensional type analysis and
type classes.},
ps = {http://www.seas.upenn.edu/~sweirich/papers/cast/cast.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/cast/cast.pdf}
}
@inproceedings{crary00,
plclub = {yes},
author = {Karl Crary and Stephanie Weirich},
title = {Resource Bound Certification},
booktitle = {Twenty-Seventh {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL})},
pages = {184--198},
year = 2000,
address = {Boston, MA, USA},
month = jan,
pdf = {http://www.seas.upenn.edu/~sweirich/papers/res/res.pdf},
ps = {http://www.seas.upenn.edu/~sweirich/papers/res/res.ps.gz},
abstract = {Various code certification systems allow the
certification and static verification of a variety of important
safety properties such as memory safety and control-flow
safety. These systems provide valuable tools for verifying that
untrusted and potentially malicious code is safe before execution.
However, one important safety property that is not usually
included is that programs adhere to specific bounds on resource
consumption, such as running time.
We present a decidable type system capable of specifying and
certifying bounds on resource consumption. Our system makes two
advances over previous resource bound certification systems, both
of which are necessary for a practical system: we allow the
execution time of programs and their subroutines to vary,
depending on their arguments, and we provide a fully automatic
compiler generating certified executables from source-level
programs. The principal device in our approach is a strategy for
simulating dependent types using sum and inductive kinds. }
}
@inproceedings{morrisett+:talx86,
plclub = {yes},
author = {Greg Morrisett and Karl Crary and Neal Glew and Dan
Grossman and Richard Samuels and Frederick Smith and
David Walker and Stephanie Weirich and Steve
Zdancewic},
title = {{TALx86}: A Realistic Typed Assembly Language},
booktitle = {Second {ACM} {SIGPLAN} Workshop on Compiler Support for System Software},
year = 1999,
month = may,
pages = {25--35},
note = {Published as {INRIA} research report number 0228, March 1999.},
address = {Atlanta, GA, USA},
ps = {http://www.seas.upenn.edu/~sweirich/papers/talx86-wcsss.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/talx86-wcsss.pdf},
abstract = {The goal of typed assembly language (TAL) is to provide
a low-level, statically typed target language that is better
suited than Java bytecodes for supporting a wide variety of
source languages and a number of important optimizations. In
previous work, we formalized idealized versions of TAL and proved
important safety properties about them. In this paper, we present
our progress in defining and implementing a realistic typed
assembly language called TALx86. The TALx86 instructions comprise
a relatively complete fragment of the Intel IA32 (32-bit 80x86
flat model) assembly language and are thus executable on
processors such as the Intel Pentium. The type system for the
language incorporates a number of advanced features necessary for
safely compiling large programs to good code.
To motivate the design of the type system, we demonstrate how
various high-level language features are compiled to TALx86. For
this purpose, we present a type-safe C-like language called
Popcorn.}
}
@inproceedings{crary+:lx,
plclub = {yes},
author = {Karl Crary and Stephanie Weirich},
title = {Flexible Type Analysis},
booktitle = {Proceedings of theFourth {ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP})},
year = 1999,
month = sep,
address = {Paris, France},
pages = {233--248},
abstract = {Run-time type dispatch enables a variety of advanced
optimization techniques for polymorphic languages, including
tag-free garbage collection, unboxed function arguments, and
flattened data structures. However, modern type-preserving
compilers transform types between stages of compilation, making
type dispatch prohibitively complex at low levels of typed
compilation. It is crucial therefore for type analysis at these
low levels to refer to the types of previous
stages. Unfortunately, no current intermediate language supports
this facility.
To fill this gap, we present the language LX, which provides a
rich language of type constructors supporting type analysis
(possibly of previous-stage types) as a programming idiom. This
language is quite flexible, supporting a variety of other
applications such as analysis of quantified types, analysis with
incomplete type information, and type classes. We also show that
LX is compatible with a type-erasure semantics.},
ps = {http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.ps.gz},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/lx/lxpaper.pdf}
}
@inproceedings{crary+:intensional,
plclub = {yes},
author = {Karl Crary and Stephanie Weirich and Greg Morrisett},
title = {Intensional Polymorphism in Type Erasure Semantics},
booktitle = {Proceedings of theThird {ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP})},
year = 1998,
address = {Baltimore, MD, USA},
month = sep,
pages = {301--313},
ps = {http://www.seas.upenn.edu/~sweirich/papers/typepass/typepass.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/typepass/typepass.pdf},
abstract = { Intensional polymorphism, the ability to dispatch to
different routines based on types at run time, enables a variety of
advanced implementation techniques for polymorphic languages,
including tag-free garbage collection, unboxed function arguments,
polymorphic marshalling, and flattened data structures. To date,
languages that support intensional polymorphism have required a
type-passing (as opposed to type-erasure) interpretation where types
are constructed and passed to polymorphic functions at run
time. Unfortunately, type-passing suffers from a number of
drawbacks; it requires duplication of constructs at the term and
type levels, it prevents abstraction, and it severely complicates
polymorphic closure conversion. We present a type-theoretic
framework that supports intensional polymorphism, but avoids many of
the disadvantages of type passing. In our approach, run-time type
information is represented by ordinary terms. This avoids the
duplication problem, allows us to recover abstraction, and avoids
complications with closure conversion. In addition, our type system
provides another improvement in expressiveness; it allows unknown
types to be refined in place thereby avoiding certain
beta-expansions required by other frameworks. }
}
@techreport{HicksW00type-loading-tr,
plclub = {yes},
author = {Michael Hicks and Stephanie Weirich},
title = {A Calculus for Dynamic Loading},
institution = {University of Pennsylvania},
year = {2000},
number = {MS-CIS-00-07},
month = {April},
pdf = { http://repository.upenn.edu/cis_reports/169/ },
abstract = {
We present the load-calculus, used to model dynamic loading, and prove it sound. The calculus extends the polymorphic lambda-calculus with a load primitive that dynamically loads terms that are closed, with respect to values. The calculus is meant to approximate the process of dynamic loading in TAL/Load , a version of Typed Assembly Language extending with dynamic linking. To model the key aspects of TAL, the calculus contains references and facilities for named types. Loadable programs may refer to named types defined by the running program, and may export new types to code loaded later. Our approach follows the framework initially outlined by Glew et. al. This calculus has been implemented in the TALx86 version of Typed Assembly Language, and is used to implement a full-featured dynamic linking library, DLpop.}
}
@incollection{hicks00,
plclub = {yes},
author = {Michael Hicks and Stephanie Weirich and Karl Crary},
title = {Safe and Flexible Dynamic Linking of Native Code},
booktitle = {Types in Compilation: Third International Workshop, TIC 2000;
Montreal, Canada, September 21, 2000; Revised Selected Papers},
editor = {R. Harper},
publisher = {Springer},
year = 2001,
series = {Lecture Notes in Computer Science},
volume = 2071,
pages = {147--176},
annote = {Related technical report: Michael Hicks and Stephanie
Weirich. A calculus for dynamic loading.
University of Pennsylvania Computer and Information Science
Technical Report,
MS-CIS-00-07, April 2000.},
abstract = {We present the design and implementation of the first
complete framework for flexible and safe dynamic linking of
native code. Our approach extends Typed Assembly Language with a
primitive for loading and typechecking code, which is flexible
enough to support a variety of linking strategies, but simple
enough that it does not significantly expand the trusted
computing base. Using this primitive, along with the ability to
compute with types, we show that we can program many existing
dynamic linking approaches. As a concrete demonstration, we have
used our framework to implement dynamic linking for a type-safe
dialect of C, closely modeled after the standard linking facility
for Unix C programs. Aside from the unavoidable cost of
verification, our implementation performs comparably with the
standard, untyped approach.},
url = {http://link.springer.de/link/service/series/0558/tocs/t2071.htm},
ps = {http://www.seas.upenn.edu/~sweirich/papers/taldynlink/taldynlink.ps.gz},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/taldynlink/taldynlink.pdf}
}
@inproceedings{flanagan96,
plclub = {yes},
author = {Cormac Flanagan and Matthew Flatt and Shriram
Krishnamurthi and Stephanie Weirich and Matthias
Felleisen},
title = {Catching Bugs in the Web of Program Invariants},
booktitle = {Proceedings of the{ACM SIGPLAN Conference on Programming Language Design
and Implementation (PLDI)}},
year = 1996,
pages = {23--32},
abstract = {MrSpidey is a user-friendly, interactive static
debugger for Scheme. A static debugger supplements the standard
debugger by analyzing the program and pinpointing those program
operations tha may cause run-time errors suce as dereferencing
the null pointer or applying non-functions. The program analysis
of MrSpidey computes value set descriptions for each term in the
program and constructs a value flow graph connecting the set
descriptions. Using the set descriptions, MrSpidey can identify
and highlight potentially erroneous program operations, whose
cause the programmer can the explore by selectively exposing
portions of the value flow graph.},
ps = {http://www.seas.upenn.edu/~sweirich/papers/pldi96-ffkwf.ps},
pdf = {http://www.seas.upenn.edu/~sweirich/papers/pldi96-ffkwf.pdf}
}
@inproceedings{NMZ12,
author = {Santosh Nagarakatte and Milo M.~K. Martin and Steve Zdancewic},
title = {Watchdog: Hardware for Safe and Secure Manual Memory
Management and Full Memory Safety},
booktitle = {Proceedings of the 39th International Symposium on Computer Architecture (ISCA)},
year = 2012,
month = jun,
hsconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/NMZ12.pdf},
abstract = {
Languages such as C and C++ use unsafe manual memory
management, allowing simple bugs (\textit{i.e.}, accesses to an object after
deallocation) to become the root cause of exploitable security
vulnerabilities. This paper proposes Watchdog, a hardware-based
approach for ensuring safe and secure manual memory management.
Inspired by prior software-only proposals, Watchdog generates a
unique identifier for each memory allocation, associates these
identifiers with pointers, and checks to ensure that the
identifier is still valid on every memory access. This use of
identifiers and checks enables Watchdog to detect errors even in
the presence of reallocations.
Watchdog stores these pointer identifiers in a disjoint shadow
space to provide comprehensive protection and ensure compatibility
with existing code.
To streamline the implementation
and reduce runtime overhead: Watchdog (1) uses micro-ops to
access metadata and perform checks, (2) eliminates metadata
copies among registers via modified register renaming, and (3)
uses a dedicated metadata cache to reduce checking overhead.
Furthermore, this paper extends Watchdog's mechanisms to detect
bounds errors, thereby providing full hardware-enforced memory
safety at low overheads.}
}
@inproceedings{OSZ12,
author = {Peter-Michael Osera and Vilhelm Sj\"{o}berg and Steve Zdancewic},
title = {Dependent Ineroperability},
booktitle = {The Sixth ACM SIGPLAN Workshop on
Programming Languages meets Program Verification (PLPV)},
year = 2012,
hconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/OSZ12.pdf},
abstract = {
In this paper we study the problem of \textit{interoperability}---combining
constructs from two separate programming languages within one program---in the
case where one of the two languages is dependently typed and the other is simply
typed. We present a core calculus called SD, which combines dependently-
and simply-typed sub-languages and supports user-defined (dependent) datatypes,
among other standard features. SD has ``boundary terms'' that mediate the
interaction between the two sub-languages. The operational semantics of SD
demonstrates how the necessary dynamic checks, which must be done when passing a
value from the simply-typed world to the dependently typed world, can be
extracted from the dependent type constructors themselves, modulo user-defined
functions for marshaling values across the boundary. We establish type-safety
and other meta-theoretic properties of SD, and contrast this approach to
others in the literature.
}
}
@inproceedings{ZNMZ12,
author = {Jianzhou Zhao and Santosh Nagarakatte and Milo M.~K. Martin and Steve Zdancewic},
title = {{Formalizing the LLVM Intermediate Representation for Verified
Program Transformations}},
booktitle = {Proc. of the {ACM} Symposium on Principles of Programming Languages (POPL)},
year = 2012,
hsconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZNMZ12.pdf},
abstract = {
This paper presents Vellvm (\textit{verified LLVM}), a framework
for reasoning about programs expressed in LLVM's intermediate
representation and transformations that operate on it. Vellvm
provides a mechanized formal semantics of LLVM's intermediate
representation, its type system, and properties of its SSA form.
The framework is built using the Coq interactive theorem prover.
It includes multiple operational semantics and proves relations among
them to facilitate different reasoning styles and proof
techniques.
To validate Vellvm's design, we extract an interpreter from the Coq
formal semantics that can execute programs from LLVM test suite and
thus be compared against LLVM reference implementations.
To demonstrate Vellvm's practicality, we formalize and verify a
previously proposed transformation that hardens C programs against
spatial memory safety violations. Vellvm's tools allow us to extract
a new, verified implementation of the transformation pass that plugs
into the real LLVM infrastructure; its performance is competitive with
the non-verified, ad-hoc original.
}
}
@inproceedings{WVPJZ11,
author = {Stephanie Weirich and Dimitrios Vytiniotis and Simon {Peyton Jones} and Steve Zdancewic},
title = {Generative Type Abstraction and Type-level Computation},
booktitle = {Proc. of the {ACM} Symposium on Principles of Programming Languages (POPL)},
year = 2011,
hsconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/WVPJZ11.pdf},
abstract = {
Modular languages support \emph{generative type abstraction},
ensuring that an abstract type is distinct from its
representation, except inside the implementation where the
two are synonymous. We show that this well-established
feature is in tension with the \emph{non-parametric features}
of newer type systems, such as indexed type families and GADTs.
In this paper we solve the problem by using kinds to
distinguish between parametric and non-parametric contexts.
The result is directly applicable to Haskell, which is rapidly
developing support for type-level computation, but the same
issues should arise whenever generativity and non-parametric features
are combined.
}
}
@inproceedings{ZZZ10,
author = {Jianzhou Zhao and Qi Zhang and Steve Zdancewic},
title = {Relational Parametricity for Polymorphic Linear Lambda Calculus},
booktitle = {Proceedings of the Eighth {ASIAN} Symposium on Programming Languages and Systems (APLAS)},
year = 2010,
hsconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZZZ10.pdf},
abstract = {
This paper presents a novel syntactic logical relation for a polymorphic
linear lambda-calculus that treats all types as linear and introduces the
constructor ! to account for intuitionistic terms, and Fo---an
extension of System F that uses kinds to distinguish linear from intuitionistic
types. We define a logical relation for open values under both open linear and
intuitionistic contexts, then extend it for open terms with evaluation and
open relation substitutions. Relations that instantiate type quantifiers are
for open terms and types. We demonstrate the applicability of this logical
relation through its soundness with respect to contextual equivalence, along
with free theorems for linearity that are difficult to achieve by closed
logical relations. When interpreting types on only closed terms, the model
defaults to a closed logical relation that is both sound and complete with
respect to contextual equivalence and is sufficient to reason about
isomorphisms of type encodings. All of our results have been mechanically
verified in Coq.
}
}
@inproceedings{NZMZ10,
author = {Santosh Nagarakatte and Jianzhou Zhao and Milo M.~K. Martin and Steve Zdancewic},
title = {{CETS}: Compiler-Enforced Temporal Safety for C},
booktitle = {Proceedings of the ACM International Symposium on Memory Management (ISMM)},
year = 2010,
hsconf = {yes},
plclub = {yes},
nsfr = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/NZMZ10.pdf},
abstract = {
Temporal memory safety errors, such as dangling pointer dereferences and
double frees, are a prevalent source of software bugs in unmanaged
languages such as C. Existing schemes that attempt to retrofit temporal
safety for such languages have high runtime overheads and/or are
incomplete, thereby limiting their effectiveness as debugging aids.
This paper presents CETS, a compile-time transformation for detecting
all violations of temporal safety in C programs. Inspired by existing
approaches, CETS maintains a unique identifier with each object,
associates this metadata with the pointers in a disjoint metadata space
to retain memory layout compatibility, and checks that the object is
still allocated on pointer dereferences. A formal proof shows that this
is sufficient to provide temporal safety even in the presence of
arbitrary casts if the program contains no spatial safety violations.
Our CETS prototype employs both temporal check removal optimizations
and traditional compiler optimizations to achieve a runtime overhead of
just 48\% on average. When combined with a
spatial-checking system, the average overall overhead is 116\%
for complete memory safety.
}
}
@inproceedings{MZ10,
author = {Karl Mazurak and Steve Zdancewic},
title = {Lolliproc: to {Concurrency from Classical Linear Logic
via Curry-Howard and Control}},
booktitle = {Proc. of the 15th ACM SIGPLAN International Conference on
Functional Programming (ICFP)},
year = 2010,
hsconf = {yes},
nsfo = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/MZ10.pdf},
abstract = {
While many type systems
based on the intuitionistic fragment of linear logic have been
proposed, applications in programming languages of the full power of
linear logic---including double-negation elimination---have remained
elusive. Meanwhile, linearity has been used in many type systems for
concurrent programs---e.g., session types---which suggests
applicability to the problems of concurrent programming, but the ways
in which linearity has interacted with concurrency primitives in
lambda calculi have remained somewhat ad-hoc. In this paper we
connect classical linear logic and concurrent functional programming
in the language Lolliproc, which provides simple primitives for
concurrency that have a direct logical interpretation and that combine
to provide the functionality of session types. Lolliproc features a
simple process calculus ``under the hood'' but hides the machinery of
processes from programmers. We illustrate Lolliproc by example and
prove soundness, strong normalization, and confluence results, which,
among other things, guarantees freedom from deadlocks and race
conditions.
}
}
@article{LZ10,
author = {Peng Li and Steve Zdancewic},
title = {{Arrows for Secure Information Flow}},
journal = {Theoretical Computer Science},
volume = {411},
number = {19},
pages = {1974-1994},
year = 2010,
publisher = {Elsevier},
plclub = {yes},
hjournal = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LZ10.pdf},
abstract = {
This paper presents an embedded security sublanguage for enforcing information-
flow policies in the standard Haskell programming language. The sublanguage pro-
vides useful information-flow control mechanisms including dynamic security lat-
tices, run-time code privileges and declassification all without modifying the base
language. This design avoids the redundant work of producing new languages, low-
ers the threshold for adopting security-typed languages, and also provides great
flexibility and modularity for using security-policy frameworks.
The embedded security sublanguage is designed using a standard combinator in-
terface called \textit{arrows}. Computations constructed in the sublanguage have static and
explicit control-flow components, making it possible to implement information-flow
control using static-analysis techniques at run time, while providing strong secu-
rity guarantees. This paper presents a formal proof that our embedded sublanguage
provides noninterference, a concrete Haskell implementation and an example appli-
cation demonstrating the proposed techniques.
}
}
@inproceedings{MZZ10,
author = {Karl Mazurak and
Jianzhou Zhao and
Steve Zdancewic},
title = {Lightweight linear types in {System} {F}$^{\circ}$},
booktitle = {ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI)},
year = 2010,
pages = {77-88},
plclub = {yes},
hconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/MZZ10.pdf},
abstract = {
We present F$^{\circ}$, an extension of System F that uses
\emph{kinds} to distinguish between linear and unrestricted types,
simplifying the use of linearity for general-purpose programming. We
demonstrate through examples how F$^{\circ}$ can elegantly express many
useful protocols, and we prove that any protocol representable
as a DFA can be encoded as an F$^{\circ}$ type. We supply
mechanized proofs of F$^{\circ}$'s
soundness and parametricity properties, along with a
nonstandard operational semantics that formalizes common intuitions
about linearity and aids in reasoning about protocols.
We compare F$^{\circ}$ to other linear systems, noting that the simplicity of our
kind-based approach leads to a more explicit account of what linearity
is meant to capture, allowing otherwise-conflicting interpretations of
linearity (in particular, restrictions on \emph{aliasing} versus
restrictions on resource \emph{usage}) to coexist peacefully.
We also discuss extensions to F$^{\circ}$ aimed at making the
core language more practical, including the additive fragment of
linear logic, algebraic datatypes, and recursion.
}
}
@inproceedings{MGLZ09,
author = {Michael J. May and
Carl A. Gunter and
Insup Lee and
Steve Zdancewic},
title = {Strong and Weak Policy Relations},
booktitle = {POLICY 2009, IEEE International Symposium on Policies for
Distributed Systems and Networks},
year = {2009},
pages = {33-36},
plclub = {yes},
hconf = {yes}
}
@inproceedings{JZ09,
author = {Limin Jia and
Steve Zdancewic},
title = {Encoding information flow in {Aura}},
booktitle = {Proceedings of the 2009 Workshop on Programming Languages
and Analysis for Security (PLAS)},
year = 2009,
pages = {17-29},
plclub = {yes},
nsfo = {yes},
hconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/JZ09.pdf},
abstract = {
Two of the main ways to protect security-sensitive
resources in computer systems are to enforce access-control policies
and information-flow policies. In this paper, we show how to enforce
information-flow policies in AURA, which is a programming
language for access control. When augmented with this mechanism for
enforcing information-flow polices, AURA can further improve the
security of reference monitors that implement access control.
We show how to encode security types
and lattices of security labels using AURA's existing constructs
for authorization logic. We prove a noninterference theorem for
this encoding. We also investigate how to use expressive
access-control policies specified in authorization logic as the policies
for information declassification.
}
}
@inproceedings{BPSW+09,
author = {Aaron Bohannon and Benjamin C. Pierce and Vilhelm Sj\"oberg and Stephanie Weirich and Steve Zdancewic},
title = {Reactive Noninterference},
booktitle = {ACM Computer and Communications Security Conference (CCS)},
year = 2009,
plclub = {yes},
hsconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/BPSW+09.pdf},
abstract = {
Many programs operate reactively---patiently waiting for user input, running
for a while producing output, and eventually returning to a state where they
are ready to accept another input (or occasionally diverging). When a
reactive program communicates with multiple parties, we would like to be
sure that it can be given secret information by one without leaking it to
others.
Motivated by web browsers and client-side web applications,
we explore definitions of noninterference for reactive programs and
identify two of special interest---one corresponding to
termination-insensitive noninterference for a simple sequential language,
the other to termination-sensitive noninterference. We focus on the former
and develop a proof technique for showing that program behaviors are secure
according to this definition. To demonstrate the viability of the approach,
we define a simple reactive language with an information-flow type system
and apply our proof technique to show that well-typed programs are secure.
}
}
@inproceedings{FPZ09,
author = {J. Nathan Foster and Benjamin C. Pierce and Steve Zdancewic},
title = {Updatable Security Views},
booktitle = {Proc. of 22nd IEEE Computer Security Foundations Symposium (CSF)},
year = 2009,
nsfo = {yes},
plclub = {yes},
hsconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/FPZ09.pdf},
abstract = {
Security views are a flexible and effective mechanism for controlling
access to confidential information. Rather than allowing untrusted
users to access source data directly, they are instead provided with a
restricted view, from which all confidential information has been
removed. The program that generates the view effectively embodies a
confidentiality policy for the underlying source data. However, this
approach has a significant drawback: it prevents users from updating
the data in the view.
To address the ``view update problem'' in general, a number of
bidirectional languages have been proposed. Programs in these
languages---often called lenses---can be run in two directions: read
from left to right, they map sources to views; from right to left,
they map updated views back to updated sources. However, existing
bidirectional languages do not deal adequately with security. In
particular, they do not provide a way to ensure the integrity of
source data as it is manipulated by untrusted users of the view.
We propose a novel framework of secure lenses that addresses these
shortcomings. We enrich the types of basic lenses with equivalence
relations capturing notions of confidentiality and integrity, and
formulate the essential security conditions as non-interference
properties. We then instantiate this framework in the domain of string
transformations, developing syntax for bidirectional string
combinators with security-annotated regular expressions as their
types.
}
}
@inproceedings{NZMZ09,
author = {Santosh Nagarakatte and Jianzhou Zhao and Milo M. K. Martin and Steve Zdancewic},
title = {{SoftBound}: {Highly Compatible and Complete Spatial Memory Safety for C}},
booktitle = {Proc. 2009 {ACM} SIGPLAN Conference on Programming Languages Design and Implementation (PLDI)},
year = 2009,
plclub = {yes},
hsconf = {yes},
nsfr = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/NZMZ09.pdf},
abstract = {
This paper proposes to combine two seemingly opposed programming
models for building massively concurrent network services: the
event-driven model and the multithreaded model. The result is a
hybrid design that offers the best of both worlds---the ease of use
and expressiveness of threads and the flexibility and performance of
events.
This paper shows how the hybrid model can be implemented entirely at
the application level using {\em concurrency monads} in Haskell,
which provides type-safe abstractions for both events and threads.
This approach simplifies the development of massively concurrent
software in a way that scales to real-world network services. The
Haskell implementation supports exceptions, symmetrical multiprocessing,
software transactional memory, asynchronous I/O mechanisms and
application-level network protocol stacks. Experimental results
demonstrate that this monad-based approach has good performance: the
threads are extremely lightweight (scaling to ten million threads),
and the I/O performance compares favorably to that of Linux NPTL.
}
}
@inproceedings{JVMZ+08,
author = {Limin Jia and Jeffrey A. Vaughan and Karl Mazurak and
Jianzhou Zhao and Luke Zarko and Joseph Schorr and Steve Zdancewic},
title = {{AURA}: {A} Programming Language for Authorization and Audit},
booktitle = {Proc. of the 13th ACM SIGPLAN International Conference on
Functional Programming (ICFP)},
year = 2008,
address = {Victoria, British Columbia, Canada},
month = sep,
hsconf = {yes},
nsfr = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/JVMZ08.pdf},
abstract = {
This paper presents AURA, a programming language for access control that
treats ordinary programming constructs (e.g., integers and recursive functions)
and authorization logic constructs (e.g., principals and access control
policies) in a uniform way.
AURA is based on polymorphic DCC and uses dependent types to
permit assertions that refer directly to AURA values while keeping
computation out of the assertion level to ensure tractability.
The main technical results of this paper include fully mechanically
verified proofs of the decidability and soundness
for AURA's type system, and a prototype typechecker and interpreter.
}
}
@inproceedings{VJMZ08,
author = {Jeffrey A. Vaughan and Limin Jia and Karl Mazurak and
Steve Zdancewic},
title = {Evidence-based Audit},
booktitle = {Proc. of 21st IEEE Computer Security Foundations Symposium (CSF)},
pages = {177--191},
year = 2008,
publisher = {{IEEE} Computer Society Press},
plclub = {yes},
nsfr = {no},
hsconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/VJMZ08.pdf},
abstract = {
Authorization logics provide a principled and flexible approach to
specifying access control policies. One of their compelling benefits
is that a proof in the logic is \emph{evidence} that an access-control
decision has been made in accordance with policy. Using such proofs
for auditing reduces the trusted computing base and enables the ability to
detect flaws in complex authorization policies. Moreover, the proof
structure is itself useful, because proof
normalization can yield information about the relevance of policy
statements. Untrusted, but well-typed, applications that access
resources through an appropriate interface must obey the access
control policy and create proofs useful for audit.
This paper presents AURA, an authorization logic based on a
dependently-typed variant of DCC and proves the metatheoretic
properties of subject-reduction and normalization. It shows the
utility of proof-based auditing in a number of examples and discusses
several pragmatic issues that must be addressed in this context.
}
}
@techreport{TZ08tr,
author = {Stephen Tse and Steve Zdancewic},
title = {Concise Concrete Syntax},
institution = {University of Pennsylvania},
year = 2008,
number = {MS-CIS-08-11},
plclub = {yes},
htr = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/TZ08tr.pdf}
}
@techreport{JVMZ+08tr,
author = {Limin Jia and Jeffrey A. Vaughan and Karl Mazurak and Jianzhou Zhao and Luke Zarko and Joseph Schorr and Steve Zdancewic},
title = {{AURA}:Preliminary Technical Results},
institution = {University of Pennsylvania},
year = 2008,
number = {MS-CIS-08-10},
plclub = {yes},
htr = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/JVMZ08tr.pdf}
}
@techreport{VJMZ08tr,
author = {Jeffrey C. Vaughan and Limin Jia and Karl Mazurak and Steve Zdancewic},
title = {Evidence-based Audit, Technical Appendix},
institution = {University of Pennsylvania},
year = 2008,
number = {MS-CIS-08-09},
plclub = {yes},
htr = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/VJMZ08tr.pdf}
}
@inproceedings{DBMZ08,
author = {Joe Devietti and Colin Blundell and Milo M.K. Martin and Steve Zdancewic},
title = {HardBound: Architectural Support for Spatial Safety of the C Programming Language},
booktitle = {International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)},
year = 2008,
month = mar,
plclub = {yes},
nsfr = {yes},
hsconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/DBMZ08.pdf},
abstract = {
The C programming language is at least as well known for its absence of
spatial memory safety guarantees (i.e., lack of bounds checking) as it is
for its high performance. C's unchecked pointer arithmetic and
array indexing allow simple programming mistakes to lead to erroneous
executions, silent data corruption, and security vulnerabilities. Many
prior proposals have tackled enforcing spatial safety in C programs by
checking pointer and array accesses. However, existing software-only
proposals have significant drawbacks that may prevent wide
adoption, including: unacceptably high runtime overheads, lack of
completeness, incompatible pointer representations, or need for
non-trivial changes to existing C source code and compiler
infrastructure.
Inspired by the promise of these software-only approaches, this paper
proposes a \textit{hardware bounded pointer} architectural primitive
that supports cooperative hardware/software enforcement of spatial
memory safety for C programs. This bounded pointer is a new hardware
primitive datatype for pointers that leaves the standard C pointer
representation intact, but augments it with bounds information
maintained separately and invisibly by the hardware. The bounds are
initialized by the software, and they are then propagated and enforced
transparently by the hardware, which automatically checks a pointer's
bounds before it is dereferenced. One mode of use requires
instrumenting only \texttt{malloc}, which enables enforcement of
per-allocation spatial safety for heap-allocated objects for existing
binaries. When combined with simple intra-procedural compiler
instrumentation, hardware bounded pointers enable a low-overhead
approach for enforcing complete spatial memory safety in unmodified C
programs.
}
}
@inproceedings{MZ07,
author = {Karl Mazurak and Steve Zdancewic},
title = {{ABash}: Finding Bugs in Bash Scripts},
booktitle = {ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS)},
year = 2007,
month = jun,
plclub = {yes},
hconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/MZ07.pdf},
abstract = {
This paper describes the design and implementation of ABash, a
tool for statically analyzing programs written in the \texttt{bash} scripting
language. Although it makes no formal guarantees against missed errors
or spurious warnings (largely due to
the highly dynamic nature of \texttt{bash} scripts), ABash is useful for
detecting certain common program errors that may lead to security
vulnerabilities. In experiments with 49 \texttt{bash} scripts taken
from popular Internet repositories,
ABash was able to identify 20 of them as containing bugs of varying
severity while yielding only a reasonable number of spurious warnings on
both these scripts and the generally bug-free initialization scripts of
the Ubuntu Linux distribution. ABash works by performing
\textit{abstract interpretation} of a \texttt{bash} script via an abstract
semantics that accounts for shell variable expansion.
The analysis is also parameterized by a collection of
signatures that describe external program interfaces (for Unix
commands, etc.), yielding an easily configurable and extensible
framework for finding bugs in \texttt{bash} scripts.
}
}
@inproceedings{VZ07,
author = {Jeffrey A. Vaughan and Steve Zdancewic},
title = {A Cryptographic Decentralized Label Model},
booktitle = {{IEEE} 2007 Symposium on Security and Privacy (Oakland)},
year = 2007,
pages = {192--206},
plclub = {yes},
hsconf = {yes},
nsfo = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/VZ07.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/VZ07.pdf},
abstract = {
Information-flow security policies are an appealing way of
specifying confidentiality and integrity policies in information
systems. Most previous work on language-based security has assumed
that programs run in a closed, managed environment and that they use
potentially unsafe constructs, such as \emph{declassification}, to
interface to external communication channels, perhaps after
encrypting data to preserve its confidentiality. This situation is
unsatisfactory for systems that need to communicate over untrusted
channels or use untrusted persistent storage, since the connection
between the cryptographic mechanisms used in the untrusted
environment and the abstract security labels used in the trusted
language environment is ad hoc and unclear.
This paper addresses this problem in three ways: First, it presents
a simple, security-typed language with a novel mechanism called
\textit{packages} that provides an abstract means for creating
opaque objects and associating them with security labels; well-typed
programs in this language enforce noninterference. Second, it shows
how to implement these packages using public-key cryptography. This
implementation strategy uses a variant of Myers and Liskov's
\textit{decentralized label model}, which supports a rich label
structure in which mutually distrusting data owners can specify
independent confidentiality and integrity requirements. Third, it
demonstrates that this implementation of packages is sound with
respect to Dolev-Yao style attackers---such an attacker cannot
determine the contents of a package without possessing the
appropriate keys, as determined by the security label on the
package.
}
}
@inproceedings{LZ07,
author = {Peng Li and Steve Zdancewic},
title = {Combining Events And Threads For Scalable Network Services},
booktitle = {Proc. 2007 {ACM} SIGPLAN Conference on Programming Languages Design and Implementation (PLDI)},
year = 2007,
pages = {189--199},
plclub = {yes},
hsconf = {yes},
nsfr = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/LZ07.ps},
abstract = {
This paper proposes to combine two seemingly opposed programming
models for building massively concurrent network services: the
event-driven model and the multithreaded model. The result is a
hybrid design that offers the best of both worlds---the ease of use
and expressiveness of threads and the flexibility and performance of
events.
This paper shows how the hybrid model can be implemented entirely at
the application level using {\em concurrency monads} in Haskell,
which provides type-safe abstractions for both events and threads.
This approach simplifies the development of massively concurrent
software in a way that scales to real-world network services. The
Haskell implementation supports exceptions, symmetrical multiprocessing,
software transactional memory, asynchronous I/O mechanisms and
application-level network protocol stacks. Experimental results
demonstrate that this monad-based approach has good performance: the
threads are extremely lightweight (scaling to ten million threads),
and the I/O performance compares favorably to that of Linux NPTL.
}
}
@inproceedings{ACZ06,
author = {Rajeev Alur and Pavol {\v C}ern{\'y} and Steve Zdancewic},
title = {Preserving Secrecy under Refinement},
booktitle = {Proc. of 33rd International Colloquium on Automata, Languages and Programming (ICALP)},
year = 2006,
pages = {107--118},
plclub = {yes},
hsconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ACZ06.pdf},
abstract = {
We propose a general framework of secrecy and
preservation of secrecy for labeled transition systems. Our
definition of secrecy is parameterized by the distinguishing power of
the observer, the properties to be kept secret, and the executions of
interest, and captures a multitude of definitions in the literature.
We define a notion of secrecy preserving refinement between
systems by strengthening the classical trace-based refinement so that
the implementation leaks a secret only when the specification also
leaks it. We show that secrecy is in general not definable in
mu-calculus, and thus not expressible in specification logics
supported by standard model-checkers. However, we develop a
simulation-based proof technique for establishing secrecy preserving
refinement. This result shows how existing refinement checkers can be
used to show correctness of an implementation with respect to a
specification.
}
}
@inproceedings{LZ06a,
author = {Peng Li and Steve Zdancewic},
title = {Encoding Information Flow in {Haskell}},
booktitle = {Proc. of 19th IEEE Computer Security Foundations Workshop (CSFW)},
year = 2006,
pages = {16--27},
publisher = {{IEEE} Computer Society Press},
plclub = {yes},
hsconf = {yes},
nsfo = {no},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LZ06a.pdf},
abstract = {
This paper presents an embedded security sublanguage for enforcing
information-flow policies in the standard Haskell programming
language. The sublanguage provides useful information-flow control
mechanisms including dynamic security lattices, run-time code
privileges and declassification, without modifying the base
language. This design avoids the redundant work of producing new
languages, lowers the threshold for adopting security-typed
languages, and also provides great flexibility and modularity for
using security-policy frameworks.
The embedded security sublanguage is designed using a standard
combinator interface called arrows. Computations constructed
in the sublanguage have static and explicit control-flow components,
making it possible to implement information-flow control using
static-analysis techniques at run time, while providing strong
security guarantees. This paper presents a concrete Haskell
implementation and an example application demonstrating the proposed
techniques.
}
}
@inproceedings{SHTZ06,
author = {Nikhil Swamy and Michael Hicks and Stephen Tse and Steve Zdancewic},
title = {Managing Policy Updates in Security-Typed Languages},
booktitle = {Proc. of 19th IEEE Computer Security Foundations Workshop (CSFW)},
year = 2006,
pages = {202--216},
publisher = {{IEEE} Computer Society Press},
plclub = {yes},
hsconf = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/SHTZ06.pdf},
abstract = {
This paper presents RX, a new security-typed
programming language with features intended to make the management of
information-flow policies more practical. Security labels in RX,
in contrast to prior approaches, are defined in terms of \emph{owned
roles}, as found in the RT role-based trust-management framework.
Role-based security policies allow flexible delegation, and our
language RX provides constructs through which programs can robustly
update policies and react to policy updates dynamically. Our dynamic
semantics use statically verified transactions to eliminate
illegal information flows across updates, which we call
transitive flows. Because policy updates can be observed
through dynamic queries, policy updates can potentially reveal
sensitive information. As such, RX considers policy statements
themselves to be potentially confidential information and subject to
information-flow metapolicies.
}
}
@article{LWZ06,
author = {Jay Ligatti and David Walker and Steve Zdancewic},
title = {A Type-theoretic Interpretation of Pointcuts and Advice},
journal = {Science of Computer Programming: Special Issue on Foundations of Aspect-Oriented Programming},
year = {2006},
pages = {240--266},
plclub = {yes},
hjournal = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LWZ06.pdf},
abstract = {
This paper defines the semantics of MinAML, an idealized
aspect-oriented programming language, by giving a type-directed
translation from a user-friendly external language to a compact,
well-defined core language. We argue that our framework is an
effective way to give semantics to aspect-oriented programming
languages in general because the translation eliminates shallow
syntactic differences between related constructs and permits
definition of a simple and elegant core language.
The core language extends the simply-typed lambda calculus with two
central new abstractions: explicitly labeled program points and
first-class advice. The labels serve both to trigger advice and to
mark continuations that the advice may return to. These constructs
are defined orthogonally to the other features of the language and
we show that our abstractions can be used in both functional and
object-oriented contexts. We prove Preservation and Progress lemmas
for our core language and show that the translation from MinAML source
into core is type-preserving. We also consider several extensions to
our basic framework including a general mechanism for analyzing the
current call stack.
}
}
@article{MSZ06,
author = {Andrew C. Myers and Andrei Sabelfeld and Steve Zdancewic},
title = {Enforcing Robust Declassification and Qualified Robustness},
journal = {Journal of Computer Security},
year = 2006,
volume = 14,
number = 2,
pages = {157--196},
plclub = {yes},
hjournal = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/MSZ06.pdf},
abstract = {
Noninterference requires that there
is no information flow from sensitive to public data in a given
system. However, many systems
release sensitive information as part of their
intended function and therefore violate noninterference.
To control information flow while permitting
information release, some systems have a downgrading or
declassification mechanism, but this creates the danger
that it may cause unintentional information release.
This paper shows that a robustness property
can be used to characterize programs in which declassification mechanisms
cannot be controlled by attackers to release more information than
intended. It describes a simple way to provably enforce this robustness
property through a type-based compile-time program analysis. The paper also
presents a generalization of robustness that
supports upgrading (endorsing) data integrity.
}
}
@article{TZ08,
author = {Stephen Tse and Steve Zdancewic},
title = {Run-time principals in information-flow type systems},
journal = {ACM Transactions on Programming Languages and Systems},
year = 2008,
volume = 30,
number = 1,
pages = 6,
plclub = {yes},
hjournal = {yes},
nsfo = {no},
pdf = {http://www.cis.upenn.edu/~stevez/papers/TZ08.pdf},
abstract = {
Information-flow type systems are a promising approach for enforcing
strong end-to-end confidentiality and integrity policies. Such
policies, however, are usually specified in terms of static
information---data is labeled _high_ or _low_ security at
compile time. In practice, the confidentiality of data may depend
on information available only while the system is running.
This paper studies language support for _run-time principals_,
a mechanism for specifying security policies that depend on which
principals interact with the system. We establish the basic
property of noninterference for programs written in such language,
and use run-time principals for specifying run-time authority in
downgrading mechanisms such as declassification.
In addition to allowing more expressive security policies, run-time
principals enable the integration of language-based security
mechanisms with other existing approaches such as Java stack
inspection and public key infrastructures. We sketch an
implementation of run-time principals via public keys such that
principal delegation is verified by certificate chains.
}
}
@inproceedings{ABFF05,
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 = {International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
year = 2005,
pages = {50--65},
hsconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ABFF05.pdf},
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-Sub, 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{HTHZ05,
author = {Michael Hicks and Stephen Tse and Boniface Hicks
and Steve Zdancewic},
title = {Dynamic updating of information-flow policies},
booktitle = {Proc. of Foundations of Computer Security Workshop (FCS)},
year = 2005,
hconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/HTHZ05.pdf},
abstract = { Applications that manipulate sensitive information
should ensure \emph{end-to-end} security by satisfying two
properties: \emph{sound execution} and some form of
\emph{noninterference}. By the former, we mean the program should
always perform actions in keeping with its current policy, and by
the latter we mean that these actions should never cause
high-security information to be visible to a low-security observer.
Over the last decade, security-typed languages have been developed
that exhibit these properties, increasingly improving so as to model
important features of real programs.
No current security-typed language, however, permits general changes
to security policies in use by running programs. This paper
presents a simple information flow type system for that allows for
dynamic security policy updates while ensuring sound execution and a
relaxed form of noninterference we term \emph{noninterference
between updates}. We see this work as an important step toward
using language-based techniques to ensure end-to-end security for
realistic applications.}
}
@inproceedings{LZ05c,
author = {Peng Li and Steve Zdancewic},
title = {{Unifying Confidentiality and Integrity in Downgrading
Policies}},
booktitle = {Proc. of Foundations of Computer Security Workshop (FCS)},
year = 2005,
hconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LZ05c.pdf},
abstract = {Confidentiality and integrity are often treated as dual
properties in formal models of information-flow control, access
control and many other areas in computer security. However, in
contrast to confidentiality policies, integrity policies are less
formally studied in the information-flow control literature. One
important reason is that traditional noninterference-based
information-flow control approaches give very weak integrity
guarantees for untrusted code. Integrity and confidentiality
policies are also different with respect to implicit information
channels.
This paper studies integrity downgrading policies in
information-flow control and compares them with their
confidentiality counterparts. We examine the drawbacks of integrity
policies based on noninterference formalizations and study the
integrity policies in the framework of downgrading policies and
program equivalences. We give semantic interpretations for
traditional security levels for integrity, namely, tainted and
untainted, and explain the interesting relations between
confidentiality and integrity in this framework. }
}
@inproceedings{Zda04,
author = {Steve Zdancewic},
title = {{Challenges for Information-flow Security}},
booktitle = {Proceedings of the 1st International Workshop on the
Programming Language Interference and Dependence (PLID'04)},
year = 2004,
note = {(5 pages)},
hinvited = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/Zda04.pdf}
}
@inproceedings{Zda03,
author = {Steve Zdancewic},
title = {{A Type System for Robust Declassification}},
booktitle = {Proceedings of the Nineteenth Conference on the
Mathematical Foundations of Programming Semantics (MFPS)},
year = 2003,
note = {(16 pages)},
month = mar,
publisher = {Electronic Notes in Theoretical Computer Science},
hinvited = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/Zda03.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/Zda03.pdf},
abstract = {Language-based approaches to information security have led to the
development of \emph{security type systems\/} that permit the
programmer to describe confidentiality policies on data. Security
type systems are usually intended to enforce \emph{noninterference},
a property that requires that high-security information not affect
low-security computation. However, in practice, noninterference is
often too restrictive---the desired policy does permit some
information leakage.
To compensate for the strictness of noninterference, practical
approaches include some mechanism for \emph{declassifying}
high-security information. But such declassification is potentially
dangerous, and its use should be restricted to prevent unintended
information leaks. Zdancewic and Myers previously introduced the
notion of \emph{robust declassification\/} in an attempt to capture
the desired restrictions on declassification, but that work did not
propose a method for determining when a program satisfies the robust
declassification condition.
This paper motivates robust declassification and shows that a simple
change to a security type system can enforce it. The idea is to
extend the lattice of security labels to include \emph{integrity}
constraints as well as confidentiality constraints and then require
that the decision to perform a declassification have high
integrity.}
}
@article{ZM02,
author = {Steve Zdancewic and Andrew C. Myers},
title = {{Secure Information Flow via Linear Continuations}},
journal = {Higher Order and Symbolic Computation},
volume = 15,
number = {2/3},
year = 2002,
pages = {209--234},
hjournal = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZM02.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZM02.pdf},
abstract = {\emph{Security-typed languages} enforce secrecy or integrity policies by
type-checking. This paper investigates continuation-passing style (CPS) as a
means of proving that such languages enforce noninterference and as a first
step towards understanding their compilation. We present a low-level, secure
calculus with higher-order, imperative features and \emph{linear
continuations}.
Linear continuations impose a stack discipline on the control flow of
programs. This additional structure in the type system lets us establish a
strong information-flow security property called \emph{noninterference}. We prove
that our CPS target language enjoys the noninterference property and we show
how to translate secure high-level programs to this low-level
language. This noninterference proof is the first of its kind for a
language with higher-order functions and state.}
}
@article{ZZNM02,
author = {Steve Zdancewic and Lantian Zheng and Nathaniel Nystrom
and Andrew C. Myers},
title = {{Secure Program Partitioning}},
journal = {Transactions on Computer Systems},
year = 2002,
volume = 20,
number = 3,
pages = {283--328},
hjournal = {yes},
plclub = {yes},
nsfo = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZZNM02.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZZNM02.pdf},
abstract = {This paper presents secure program partitioning, a language-based
technique for protecting confidential data during computation in
distributed systems containing mutually untrusted hosts. Confidentiality
and integrity policies can be expressed by annotating programs with
security types that constrain information flow; these programs can then
be partitioned automatically to run securely on heterogeneously trusted
hosts. The resulting communicating subprograms collectively implement
the original program, yet the system as a whole satisfies the security
requirements of participating principals without requiring a universally
trusted host machine. The experience in applying this methodology and
the performance of the resulting distributed code suggest that this is a
promising way to obtain secure distributed computation.
This article is an expanded version of the published paper ``Untrusted
Hosts and Confidentiality: Secure Program Partitioning''.
The main difference between the two is Appendix A, which
contains a correctness proof for the control-transfer protocols described
in Section 5.}
}
@article{GMZ00,
author = {Dan Grossman and Greg Morrisett and Steve Zdancewic},
title = {{Syntactic Type Abstraction}},
journal = {Transactions on Programming Languages and Systems},
year = 2000,
volume = 22,
number = 6,
pages = {1037--1080},
month = nov,
hjournal = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/GMZ00.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/GMZ00.pdf},
abstract = {Software developers often structure programs in such a
way that different pieces of code constitute distinct
principals. Types help define the protocol by which these principals
interact. In particular, abstract types allow a principal to make
strong assumptions about how well-typed clients use the facilities
that it provides. We show how the notions of principals and type
abstraction can be formalized within a language. Different principals
can know the implementation of different abstract types. We use
additional syntax to track the flow of values with abstract types
during the evaluation of a program and demonstrate how this framework
supports syntactic proofs (in the style of subject reduction) for
type-abstraction properties. Such properties have traditionally
required semantic arguments; using syntax avoids the need to build a
model for the language. We present various typed lambda calculi with
principals, including versions that have mutable state and recursive types.}
}
@inproceedings{TZ05a,
author = {Stephen Tse and Steve Zdancewic},
title = {{Designing a Security-typed Language with Certificate-based Declassification}},
booktitle = {Proc. of the 14th European Symposium on Programming (ESOP)},
year = 2005,
volume = 3444,
pages = {279--294},
hsconf = {yes},
plclub = {yes},
nsfo = {no},
pdf = {http://www.cis.upenn.edu/~stevez/papers/TZ05a.pdf},
abstract = {This paper presents a calculus that supports information-flow
security policies and certificate-based declassification. The
decentralized label model and its downgrading mechanisms are
concisely expressed in the polymorphic lambda calculus with
subtyping (System F-Sub). We prove a conditioned version of the
noninterference theorem such that authorization for declassification
is justified by digital certificates from public-key
infrastructures.}
}
@inproceedings{LZ05b,
author = {Peng Li and Steve Zdancewic},
title = {{Practical Information-flow Control in Web-based Information Systems}},
booktitle = {Proc. of 18th IEEE Computer Security Foundations Workshop (CSFW)},
year = 2005,
pages = {2--15},
hsconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LZ05b.pdf},
abstract = {This paper presents a practical application of
language-based information-flow control, namely, a domain-specific
web scripting language designed for interfacing with databases. The
primary goal is to provide strong enforcement of confidentiality and
integrity policies: confidential data can be released only in
permitted ways and trustworthy data must result from expected
computations or conform to expected patterns. Such security
policies are specified in the database layer and statically enforced
for the rest of the system in an end-to-end fashion.
In contrast with existing web-scripting languages, which provide
only ad hoc mechanisms for information security, the scripting
language described here uses principles based on the well-studied
techniques in information-flow type systems. However, because web
scrips often need to downgrade confidential data and manipulate
untrusted user input, they require practical and convenient ways of
downgrading secure data. To achieve this goal, the language allows
safe downgrading according to \emph{downgrading policies} specified
by the programmer. This novel, pattern-based approach provides a
practical instance of recent work on \emph{delimited release} and
\emph{relaxed noninterference} and extends that work by accounting
for integrity policies. }
}
@inproceedings{LZ05,
author = {Peng Li and Steve Zdancewic},
title = {{Downgrading Policies and Relaxed Noninterference}},
booktitle = {Proc. 32nd {ACM} Symp. on Principles of Programming
Languages (POPL)},
year = 2005,
pages = {158--170},
month = jan,
hsconf = {yes},
plclub = {yes},
nsfo = {no},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LZ05a.pdf},
abstract = { In traditional information-flow type systems, the
security policy is often formalized as noninterference properties.
However, noninterference alone is too strong to express security
properties useful in practice. If we allow downgrading in such
systems, it is challenging to formalize the security policy as an
extensional property of the system.
This paper presents a generalized framework of downgrading
policies. Such policies can be specified in a simple and tracable
language and can be statically enforced by mechanisms such as type
systems. The security guarantee is then formalized as a concise
extensional property using program equivalences. This
\textit{relaxed noninterference} generalizes traditional pure
noninterference and precisely characterizes the information released
due to downgrading.
}
}
@inproceedings{MSZ04,
author = {Andrew C. Myers and Andrei Sabelfeld and Steve Zdancewic},
title = {Enforcing Robust Declassification},
booktitle = {Proc. of 17th IEEE Computer Security Foundations Workshop (CSFW)},
pages = {172--186},
year = 2004,
hsconf = {yes},
plclub = {yes},
nsfr = {no},
pdf = {http://www.cis.upenn.edu/~stevez/papers/MSZ04.pdf},
abstract = {Noninterference requires that there is no information
flow from sensitive to public data in a given system. However, many
systems perform intentional release of sensitive information as part
of their correct functioning and therefore violate noninterference.
To control information flow while permitting intentional information
release, some systems have a downgrading or declassification
mechanism. A major danger of such a mechanism is that it may cause
unintentional information release. This paper shows that a
robustness property can be used to characterize programs in which
declassification mechanisms cannot be exploited by attackers to
release more information than intended. It describes a simple way
to provably enforce this robustness property through a type-based
compile-time program analysis. The paper also presents a
generalization of robustness that supports upgrading (endorsing)
data integrity.}
}
@inproceedings{LZ04a,
author = {Peng Li and Steve Zdancewic},
title = {{Advanced Control Flow in Java Card Programming}},
booktitle = {Proceedings of the 2004 ACM SIGPLAN/SIGBED Conference on Languages,
Compilers, and Tools for Embedded Systems (LCTES)},
pages = {165--174},
year = 2004,
month = jun,
hsconf = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LZ04a.pdf},
abstract = {
Java Card technology simplifies the development of smart card
applications by providing a high-level programming language similar to
Java. However, the master-slave programming model used in current
Java Card platform creates control flow difficulties when writing
complex card programs, making it inconvenient, tedious, and
error-prone to implement Java Card applications. This paper examines
these drawbacks of the master-slave model and proposes a concurrent
thread model for developing future Java Card programs, which is much
closer to conventional Java network programming. This paper also
presents a code translation algorithm and a corresponding tool that
makes it possible to write card programs in the concurrent thread
model without losing compatibility with the existing Java Card API.
}
}
@inproceedings{TZ04a,
author = {Stephen Tse and Steve Zdancewic},
title = {{Run-time Principals in Information-flow Type Systems}},
booktitle = {IEEE 2004 Symposium on Security and Privacy (Oakland)},
year = 2004,
pages = {179--193},
month = may,
publisher = {{IEEE} Computer Society Press},
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/TZ04a.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/TZ04a.pdf},
abstract = {
Information-flow type systems are a promising approach for enforcing
strong end-to-end confidentiality and integrity policies. Such
policies, however, are usually specified in term of static
information--data is labeled \textit{high} or \textit{low} security at
compile time. In practice, the confidentiality of data may depend
on information available only while the system is running
This paper studies language support for \textit{run-time principals}, a
mechanism for specifying information-flow security policies that
depend on which principals interact with the system. We establish
the basic property of noninterference for programs written in such
language, and use run-time principals for specifying run-time
authority in downgrading mechanisms such as declassification.
In addition to allowing more expressive security policies, run-time
principals enable the integration of language-based security
mechanisms with other existing approaches such as Java stack
inspection and public key infrastructures. We sketch an
implementation of run-time principals via public keys such that
principal delegation is verified by certificate chains.
}
}
@inproceedings{LMZ03,
author = {Peng Li and Yun Mao and Steve Zdancewic},
title = {{Information Integrity Policies}},
booktitle = {Proceedings of the Workshop on Formal Aspects in Security \& Trust (FAST)},
year = 2003,
month = sep,
hconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/LMZ03.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/LMZ03.pdf},
abstract = {Information integrity policies are traditionally enforced by
access control mechanisms that prevent unauthorized users from
modifying data. However, access control does not provide end-to-end
assurance of integrity. For that reason, integrity guarantees in
the form of noninterference assertions have been proposed. Despite
the appeals of such information-flow based approaches to integrity,
that solution is also unsatisfactory because it leads to a weaker
notion of integrity than needed in practice.
This paper attempts to clarify integrity policies by
comparing and contrasting access control vs. information flow,
integrity vs. confidentiality policies, and
integrity vs. availability policies. The paper also examines data
invariants as a way to strengthen integrity. The result is a better
classification of information-integrity policies.}
}
@inproceedings{WZL03,
author = {David Walker and Steve Zdancewic and Jay Ligatti},
title = {{A Theory of Aspects}},
booktitle = {Proc. of the 8th ACM SIGPLAN International Conference on
Functional Programming (ICFP)},
year = 2003,
pages = {127--139},
address = {Upsala, Sweden},
month = aug,
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/WZL03.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/WZL03.pdf},
abstract = {This paper define the semantics of MinAML, an idealized
aspect-oriented programming language, by giving
a type-directed translation from its user-friendly external language
to its compact, well-defined core language.
We argue that our framework is an effective way
to give semantics to aspect-oriented programming languages in
general because the translation eliminates shallow syntactic differences
between related constructs and permits definition of a clean,
easy-to-understand, and easy-to-reason-about core language.
The core language extends the simply-typed lambda
calculus with two central new abstractions: explicitly labeled program
points and first-class advice. The labels serve both to trigger
advice and to mark continuations that the advice may return to. These
constructs are defined orthogonally to the other features of the
language and we show that our abstractions can be used in both
functional and object-oriented contexts. The labels are well-scoped
and the language as a whole is well-typed. Consequently, programmers
can use lexical scoping in the standard way to prevent aspects from
interfering with local program invariants.
}
}
@inproceedings{SSDK03,
author = {Usa Sammapun and Raman Sharykin and Margaret Delap and Myong Kim and Steve Zdancewic},
title = {{Formalizing {Java-MaC}}},
booktitle = {Proceedings of the Third Runtime Verification Workshop},
publisher = {Electronic Notes in Theoretical Computer Science},
year = 2003,
pages = {171--190},
month = jul,
hconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/SSDK03.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/SSDK03.pdf},
abstract = {The Java-MaC framework is a run-time verification system for Java
programs that can be used to dynamically test and enforce safety
policies. This paper presents a formal model of the Java-MaC safety
properties in terms of an operational semantics for Middleweight
Java, a realistic subset of full Java. This model is intended to be
used as a framework for studying the correctness of Java-MaC program
instrumentation, optimizations, and future experimentation with
run-time monitor expressiveness. As a preliminary demonstration of this model's
applicability for these tasks, the paper sketches a correctness result
for a simple program instrumentation scheme.
}
}
@inproceedings{ZM03,
author = {Steve Zdancewic and Andrew C. Myers},
title = {{Observational Determinism for Concurrent Program Security}},
booktitle = {Proc. of 16th IEEE Computer Security Foundations Workshop (CSFW)},
year = 2003,
pages = {29--45},
month = jul,
address = {Asilomar, CA},
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZMO3.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZMO3.pdf},
abstract = {Noninterference is a property of sequential programs that is useful
for expressing security policies for data confidentiality and
integrity. However, extending noninterference to concurrent programs has
proved problematic. In this paper we present a relatively expressive
secure concurrent language. This language, based on existing
concurrent calculi, provides first-class channels, higher-order
functions, and an unbounded number of threads. Well-typed programs
obey a generalization of noninterference that ensures
immunity to internal
timing attacks and to attacks that exploit information about the thread
scheduler. Elimination of these refinement attacks is possible because
the enforced security property extends noninterference with
observational determinism. Although the security property is strong,
it also avoids some of the restrictiveness imposed on
previous security-typed concurrent languages.
}
}
@inproceedings{GGKS03,
author = {Michael Greenwald and Carl A. Gunter and Bj\"{o}rn Knutsson and
Andre Scedrov and Jonathan M. Smith and Steve Zdancewic},
title = {{Computer Security is Not a Science (but it should be)}},
booktitle = {Proceedings of the Large-Scale Network Security Workshop},
year = 2003,
month = mar,
hconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/GGKS03.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/GGKS03.pdf}
}
@inproceedings{ZCZM03,
author = {Lantian Zheng and Stephen Chong and Steve Zdancewic
and Andrew C. Myers},
title = {{Building Secure Distributed Systems Using Replication and
Partitioning}},
booktitle = {{IEEE} 2003 Symposium on Security and Privacy (Oakland)},
year = 2003,
pages = {236--250},
publisher = {{IEEE} Computer Society Press},
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZCZM03.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZCZM03.pdf},
abstract = {A challenging unsolved security problem is how to
specify and enforce system-wide security policies; this problem is
even more acute in distributed systems with mutual distrust. This
paper describes a way to enforce policies for data confidentiality and
integrity in such an environment. Programs annotated with security
specifications are statically checked and then transformed by the
compiler to run securely on a distributed system with untrusted
hosts. The code and data of the computation are partitioned across the
available hosts in accordance with the security specification. The
key contribution is automatic replication of code and data to increase
assurance of integrity---without harming confidentiality, and without
placing undue trust in any host. The compiler automatically generates
secure run-time protocols for communication among the replicated code
partitions. Results are given from a prototype implementation applied
to various distributed programs. }
}
@inproceedings{ZZNM01,
year = 2001,
author = {Steve Zdancewic and Lantian Zheng and Nathaniel Nystrom
and Andrew C. Myers},
title = {{Untrusted Hosts and Confidentiality: Secure Program Partitioning}},
series = {Operating Systems Review},
booktitle = {Proc. 18th {ACM} Symp. on Operating System Principles (SOSP)},
address = {Banff, Canada},
month = oct,
volume = {35(5)},
pages = {1--14},
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZZNM01.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZZNM01.pdf},
abstract = {This paper presents secure program partitioning, a
language-based technique for protecting confidential data during
computation in distributed systems containing mutually untrusted
hosts. Confidentiality and integrity policies can be expressed by
annotating programs with security types that constrain information
flow; these programs can then be partitioned automatically to run
securely on heterogeneously trusted hosts. The resulting
communicating subprograms collectively implement the original
program, yet the system as a whole satisfies the security
requirements of participating principals without requiring a
universally trusted host machine. The experience in applying this
methodology and the performance of the resulting distributed code
suggest that this is a promising way to obtain secure distributed
computation. }
}
@inproceedings{ZM01b,
author = {Steve Zdancewic and Andrew C. Myers},
title = {{Robust Declassification}},
booktitle = {Proc. of 14th IEEE Computer Security Foundations Workshop (CSFW)},
month = jun,
year = 2001,
address = {Cape Breton, Canada},
pages = {15--23},
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZM01b.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZM01b.pdf},
abstract = { Security properties based on information flow, such as
noninterference, provide strong guarantees that confidentiality is
maintained. However, programs often need to leak some amount of
confidential information in order to serve their intended purpose,
and thus violate noninterference. Real systems that control
information flow often include mechanisms for downgrading or
declassifying information; however, declassification can easily
result in the unexpected release of confidential information.
This paper introduces a formal model of information flow in systems
that include intentional information leaks and shows how to
characterize what information leaks. Further, we define a notion of
robustness for systems that include information leaks introduced by
declassification. Robust systems have the property that an attacker is
unable to exploit declassification channels to obtain more
confidential information than was intended to be released. We show
that all systems satisfying a noninterference-like property are
robust; for other systems, robustness involves a nontrivial
interaction between confidentiality and integrity properties. We
expect this model to provide new tools for the characterization of
information flow properties in the presence of intentional information
leaks. }
}
@inproceedings{ZM01,
author = {Steve Zdancewic and Andrew C. Myers},
title = {{Secure Information Flow and {CPS}}},
booktitle = {Proc. of the 10th European Symposium on Programming (ESOP)},
year = 2001,
volume = 2028,
month = apr,
series = {Lecture Notes in Computer Science},
pages = {46--61},
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZM01.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZM01.pdf},
abstract = {Security-typed languages enforce secrecy or integrity
policies by type-checking. This paper investigates
continuation-passing style as a means of proving that such languages
enforce non-interference and as a first step towards understanding
their compilation. We present a low-level, secure calculus with
higher-order, imperative features. Our type system makes novel use
of ordered linear continuations.}
}
@inproceedings{ZGM99,
author = {Steve Zdancewic and Dan Grossman and Greg Morrisett},
title = {{Principals in Programming Languages: A Syntactic Proof Technique}},
booktitle = {Proc. of the 4th ACM SIGPLAN International Conference on
Functional Programming (ICFP)},
year = 1999,
pages = {197--207},
address = {Paris, France},
month = sep,
hsconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZGM99.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZGM99.pdf},
abstract = {Programs are often structured around the idea that
different pieces of code comprise distinct principals, each with a
view of its environment. Typical examples include the modules of a
large program, a host and its clients, or a collection of
interactive agents.
In this paper, we formalize this notion of principal in the
programming language itself. The result is a language in which
intuitive statements such as, ``the client must call open to obtain a
file handle'', can be phrased and proven formally.
We add principals to variants of the simply-typed lambda-calculus and
show how we can track the code corresponding to each principal
throughout evaluation. This multiagent calculus yields syntactic
proofs of some type abstraction properties that traditionally require
semantic arguments.}
}
@inproceedings{MCGG99,
author = {Greg Morrisett and Karl Crary and Neal Glew and Dan
Grossman and Richard Samuels and Frederick Smith and David
Walker and Stephanie Weirich and Steve Zdancewic},
title = {{{TALx86}: A Realistic Typed Assembly Language}},
booktitle = {2nd {ACM SIGPLAN} Workshop on Compiler Support for
System Software},
year = 1999,
pages = {25--35},
hconf = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/MCGG99.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf},
abstract = {The goal of typed assembly language (TAL) is to provide
a low-level, statically typed target language that is better suited
than Java bytecodes for supporting a wide variety of source
languages and a number of important optimizations. In previous work,
we formalized idealized versions of TAL and proved important safety
properties about them. In this paper, we present our progress in
defining and implementing a realistic typed assembly language called
TALx86. The TALx86 instructions comprise a relatively complete
fragment of the Intel IA32 (32-bit 80x86 flat model) assembly
language and are thus executable on processors such as the Intel
Pentium. The type system for the language incorporates a number of
advanced features necessary for safely compiling large programs to
good code.
To motivate the design of the type system, we demonstrate how various
high-level language features are compiled to TALx86. For this purpose,
we present a type-safe C-like language called Popcorn.}
}
@techreport{TZ05atr,
author = {Stephen Tse and Steve Zdancewic},
title = {{Designing a Security-typed Language with Certificate-based Declassification}},
institution = {University of Pennsylvania},
number = {MIS-CIS-04-16},
year = 2004,
htr = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/TZ05atr.pdf},
abstract = {This paper presents the design of a programming language that
supports information-flow security policies and certificate-based
declassification.
The language uses monadic information-flow annotations in the style
of Abadi et al.'s dependency core calculus, and has an effects
system and fixpoints. The type system conflates security concepts
such as labels, principals, and privileges with abstract types,
allowing a uniform treatment of lattice structures throughout the
language. Myers' and Liskov's decentralized label model is encoded
using type constructors that describe confidentiality and integrity
policies, and label refinements and principal groups follow
naturally from intersection and union types. Singleton types,
combined with bounded universal and existential quantifications,
connect the type system with public-key infrastructures whose
digital certificates provide authorization for privileged operations
such as declassification. These features allow specification of
security policies in term of dynamic entities such as run-time user
identities and file access permissions.
Besides showing that the language is sound, we present a security
theorem that generalizes standard noninterference to account for
information flows introduced by declassification. Although this
result gives only a coarse approximation to the information
potentially leaked, it captures our intuitions about
certificate-based declassification.
}
}
@techreport{TZ04c,
author = {Stephen Tse and Steve Zdancewic},
title = {{Translating Dependency into Parametricity}},
institution = {University of Pennsylvania},
year = 2004,
number = {MIS-CIS-04-01},
htr = {yes},
plclub = {yes},
pdf = {http://www.cis.upenn.edu/~stevez/papers/TZ04btr.pdf},
abstract = {
The \textit{dependency core calculus} (DCC) was introduced by Abadi
et al. as a unifying formal framework in which to study a variety of
important program analyses including binding-time, information-flow,
slicing, and function call tracking. The novel feature of DCC is a
lattice of monads and a nonstandard typing rule for their associated
\texttt{bind} operations. Intuitively, the lattice structure describes
which computations in a program may depend on each other. Abadi et
al. prove a \textit{noninterference} result that establishes the
correctness of DCC's type system, and they use that result to show
that type systems for the above-mentioned analyses are correct.
In this paper, we study the relationship between DCC and the
Girard--Reynolds polymorphic lambda calculus (System F). In
particular, we show how to encode the recursion-free fragment of DCC
into F via a type-directed translation. The main theorem we present
uses this translation to derive the noninterference result for DCC
from the standard parametricity theorem of System F. In addition to
providing insight into DCC's type system, the hope is that the
translation presented here may yield implementation strategies for
non-standard type systems (e.g. for information flow security) in
languages that have parametric polymorphism.
}
}
@techreport{TZ03,
author = {Stephen Tse and Steve Zdancewic},
title = {{Run-time Principals in Information-flow Type Systems}},
institution = {University of Pennsylvania},
year = 2003,
number = {MS-CIS-03-39},
note = {The conference version appears in {IEEE} Security and Privacy 2004},
htr = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/TZ03.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/TZ03.pdf},
abstract = {
Information-flow type systems are a promising approach for enforcing
strong end-to-end confidentiality and integrity policies. Such
policies, however, are usually specified in term of static
information--data is labeled \textit{high} or \textit{low} security at
compile time. In practice, the confidentiality of data may depend
on information available only while the system is running
This paper studies language support for \textit{run-time principals}, a
mechanism for specifying information-flow security policies that
depend on which principals interact with the system. We establish
the basic property of noninterference for programs written in such
language, and use run-time principals for specifying run-time
authority in downgrading mechanisms such as declassification.
In addition to allowing more expressive security policies, run-time
principals enable the integration of language-based security
mechanisms with other existing approaches such as Java stack
inspection and public key infrastructures. We sketch an
implementation of run-time principals via public keys such that
principal delegation is verified by certificate chains.
}
}
@techreport{ZZNM01b,
year = 2001,
title = {{Secure Program Partitioning}},
author = {Steve Zdancewic and Lantian Zheng and Nathaniel Nystrom
and Andrew C. Myers},
institution = {Computer Science Dept., Cornell University},
number = {2001-1846},
htr = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZZNM01b.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZZNM01b.pdf},
abstract = {This paper presents secure program partitioning, a
language-based technique for protecting confidential data during
computation in distributed systems containing mutually untrusted
hosts. Confidentiality and integrity policies can be expressed by
annotating programs with security types that constrain information
flow; these programs can then be partitioned automatically to run
securely on heterogeneously trusted hosts. The resulting
communicating subprograms collectively implement the original
program, yet the system as a whole satisfies the security
requirements of participating principals without requiring a
universally trusted host machine. The experience in applying this
methodology and the performance of the resulting distributed code
suggest that this is a promising way to obtain secure distributed
computation.
This Technical Report is an expanded version of the published paper
``Untrusted Hosts and Confidentiality: Secure Program Partitioning''.
The main difference between the two is Appendix A, which contains a
correctness proof for the control-transfer protocols described in
Section 5.}
}
@techreport{ZM00,
author = {Steve Zdancewic and Andrew C. Myers},
title = {{Confidentiality and Integrity with Untrusted Hosts}},
institution = {Computer Science Dept., Cornell University},
year = 2000,
number = {2000-1810},
htr = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZM00.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZM00.pdf},
abstract = {Several \emph{security-typed languages} have recently been proposed to enforce
security properties such as confidentiality or integrity by type checking.
We propose a new security-typed language, Spl@, that
addresses two important limitations of previous approaches.
First, existing languages assume that the underlying execution platform
is trusted; this assumption does not scale to distributed computation in
which a variety of differently trusted hosts are available to execute
programs. Our new approach, \emph{secure program partitioning}, translates
programs written assuming complete trust in a single executing host into
programs that execute using a collection of variously trusted hosts to
perform computation. As the trust configuration of a distributed system
evolves, this translation can be performed as necessary for security.
Second, many common program transformations do not work in existing
security-typed languages; although they produce equivalent
programs, these programs are rejected because of \emph{apparent} information
flows. Spl@ uses a novel mechanism
based on \emph{ordered linear continuations} to permit a richer class of program
transformations, including secure program partitioning.}
}
@techreport{ZG99,
author = {Steve Zdancewic and Dan Grossman},
title = {{Principals in Programming Languages: Technical Results}},
institution = {Computer Science Dept., Cornell University},
year = 1999,
number = {TR99-1752},
month = jun,
htr = {yes},
plclub = {yes},
ps = {http://www.cis.upenn.edu/~stevez/papers/ZG99.ps},
pdf = {http://www.cis.upenn.edu/~stevez/papers/ZG99.pdf},
abstract = {This is the companion technical report for ``Principals
in Programming Languages: A Syntactic Proof Technique.'' See that
document for a more readable version of these results.
In this paper, we describe two variants of the simply typed
lambda-calculus extended with a notion of principal. The results are
languages in which intuitive statements like ``the client must call
open to obtain a file handle'' can be phrased and proven formally.
The first language is a two-agent calculus with references and
recursive types, while the second language explores the possibility of
multiple agents with varying amounts of type information. We use these
calculi to give syntactic proofs of some type abstraction results that
traditionally require semantic arguments. }
}