Jonathan Chan and Stephanie Weirich.
Stratified Type Theory.
In Viktor Vafeiadis, editor, European Symposium on Programming
Languages and Systems, ESOP 2025, May 2025.
To Appear.
[ bib ]
Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey
Velez-Ginorio, and Stephanie Weirich.
Effects and Coeffects in Call-By-Push-Value.
Proc. ACM Program. Lang., 8(OOPSLA), October 2024.
To Appear.
[ bib ]
Li-Yao Xia, Laura Israel, Maite Kramarz, Nathan Coltharp, Koen Claessen,
Stephanie Weirich, and Yao Li.
Story of Your Lazy Function’s Life: A Bidirectional Demand
Semantics for Mechanized Cost Analysis of Lazy Programs.
Proc. ACM Program. Lang., 8(ICFP), August 2024.
[ bib |
DOI |
.pdf ]
Stephen Mell, Steve Zdancewic, and Osbert Bastani.
Optimal Program Synthesis via Abstract Interpretation.
8(POPL), 2024.
[ bib |
.pdf ]
Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich.
Internalizing Indistinguishability with Dependent Types.
Proc. ACM Program. Lang., 8(POPL), January 2024.
[ bib |
DOI |
.pdf ]
Stephanie Weirich.
Tracking how dependently-typed functions use their arguments,
2024.
Invited keynote at LICS/ICALP/FSCD.
[ bib ]
Harrison Goldstein, Jeffrey Tao, Zac Hatfield-Dodds, Benjamin C. Pierce, and
Andrew Head.
Lucid Property-Based Testing, 2024.
Under submission.
[ bib |
.pdf ]
Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and
Andrew Head.
Property-Based Testing in Practice.
In Proceedings of the IEEE/ACM 46th International
Conference on Software Engineering, volume 187 of ICSE ’24,
pages 1–13, Lisbon, Portugal, 2024. Association for Computing Machinery.
[ bib |
DOI |
http ]
Benjamin C. Pierce, January 2024.
Short talk at POPL reception.
[ bib |
slides ]
Benjamin C. Pierce.
delta: Ordered Types for Stream Processing, January 2024.
Talk at Trends in Functional Programming (TFP).
[ bib |
slides ]
Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and
Andrew Head.
Property-Based Testing in Practice.
In International Conference on Software Engineering (ICSE),
2024.
[ bib |
.pdf ]
Joseph W. Cutler, Christopher Watson, Phillip Hilliard, Harrison Goldstein,
Caleb Stanford, and Benjamin C. Pierce.
Stream Types.
Proceedings of the ACM on Programming Languages, (PLDI), 2024.
To appearJ. W. Cutler, C. Watson, P. Hilliard, H. Goldstein, C.
Stanford, and B. C. Pierce, “Stream types,” Proceed- ings of the ACM on
Programming Languages, no. PLDI, 2024. To appear.
[ bib |
http ]
Harrison Goldstein, Samantha Frohlich, Meng Wang, and Benjamin C. Pierce.
Reflecting on Random Generation.
Proceedings of the ACM on Programming Languages, (ICFP), 2024.
To appear.
[ bib ]
Harrison Goldstein.
Tyche: In Situ Exploration of Random Testing
Effectiveness (Demo), October 2023.
[ bib |
.pdf ]
Yiyun Liu and Stephanie Weirich.
Dependently-Typed Programming with Logical Equality Reflection.
Proc. ACM Program. Lang., 7(ICFP), August 2023.
[ bib |
DOI |
.pdf ]
Benjamin C. Pierce.
What Does Subtyping Mean?, August 2023.
Talk at Programming Languages Mentoring Workshop (PLMW).
[ bib |
slides ]
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco
Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg,
Andrew Tolmach, and Brent Yorgey.
Programming Language Foundations.
Software Foundations series, volume 2. Electronic textbook, May 2023.
Version 6.6. http://www.cis.upenn.edu/ bcpierce/sf.
[ bib ]
Harrison Goldstein, Samantha Frohlich, Benjamin C. Pierce, and Meng Wang.
Reflecting on Random Generation, February 2023.
Under submission.
[ bib ]
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic.
Choice Trees: Representing Nondeterministic, Recursive, and
Impure Programs in Coq.
Proceedings of the ACM on Programming Languages, 7(POPL), 2023.
[ bib |
.pdf ]
Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliviera, and Steve Zdancewic.
A Bowtie for a Beast: Overloading, Eta Expansion, and
Extensible Data Types in F.
Proceedings of the ACM on Programming Languages, 7(POPL), 2023.
[ bib |
.pdf ]
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic.
Semantics for Noninterference with Interaction Trees.
In Proceedings of the 37th Annual European Conference on
Object-Oriented Programming (ECOOP 2023), 2023.
[ bib |
.pdf ]
Stephen Mell, Favyen Bastani, Steve Zdancewic, and Osbert Bastani.
Synthesizing Trajectory Queries from Examples.
In Computer Aided Verification - 35th International Conference,
CAV, 2023.
[ bib |
.pdf ]
Lawrence Dunn, Val Tannen, and Steve Zdancewic.
Tealeaves: Structured Monads for Generic First-Order Abstract
Syntax Infrastructure.
In 14th International Conference on Interactive Theorem Proving
(ITP), 2023.
[ bib |
.pdf ]
Stephanie Weirich.
Implementing Dependent Types in pi-forall, 2023.
Lecture notes for the Oregon Programming Languages Summer School.
[ bib |
DOI |
http ]
Jessica Shi, Alperen Keles, Harrison Goldstein, Benjamin C Pierce, and Leonidas
Lampropoulos.
Etna: An Evaluation Platform for Property-Based Testing
(Experience Report).
Proceedings of the ACM on Programming Languages,
7(ICFP):878–894, 2023.
[ bib ]
Joseph W. Cutler, Christopher Watson, Phillip Hilliard, Harrison Goldstein,
Caleb Stanford, and Benjamin C. Pierce.
Stream Types, 2023.
[ bib |
arXiv |
http ]
Joseph W. Cutler, Christopher Watson, Phillip Hilliard, Harrison Goldstein,
Caleb Stanford, and Benjamin C. Pierce.
Stream Types, 2023.
[ bib |
arXiv |
http ]
Jessica Shi, Benjamin Pierce, and Andrew Head.
Towards a Science of Interactive Proof Reading.
In 13th annual workshop on the intersection of HCI and PL
(PLATEAU), 2023.
[ bib ]
Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce,
and Andrew Tolmach.
Stack Safety as a Security Property.
In IEEE Symposium on Computer Security Foundations (CSF). IEEE
Computer Society Press, 2023.
[ bib ]
Harrison Goldstein, Joseph W. Cutler, Adam Stein, Benjamin C. Pierce, and
Andrew Head.
Some Problems with Properties.
In Workshop on Human Aspects of Types and Reasoning Assistants
(HATRA), volume 1, December 2022.
[ bib |
.pdf ]
Yao Li and Stephanie Weirich.
Program Adverbs and Tlön Embeddings.
Proc. ACM Program. Lang., 6(ICFP), September 2022.
Distinguished Paper Award. Artifact available.
[ bib |
DOI |
.pdf ]
Benjamin C. Pierce.
Imagining the Reader, July 2022.
Talk at Programming Languages Mentoring Workshop (PLMW).
[ bib |
slides ]
Benjamin C. Pierce.
Software Foundations, 15 years on, July 2022.
Talk at Newton Institute workshop on Formal Education.
[ bib |
slides ]
Yao Li and Stephanie Weirich.
Program Adverbs and Tlön Embeddings (artifact).
Technical report, June 2022.
Awarded “Available” and “Evaluated & Reusable” badges by ICFP
2023 Artifact Evaluation Committee.
[ bib |
DOI ]
Benjamin C. Pierce.
Understanding Property-Based Testing by Talking to People, May
2022.
Short talk at Working Group 2.8.
[ bib |
slides ]
Benjamin C. Pierce.
(When) Will Property-Based Testing Rule The World?, May 2022.
Keynote at Yow! Lambda Jam Conference.
[ bib |
slides ]
Joseph Cutler, Harrison Goldstein, Koen Claessen, John Hughes, and Benjamin C.
Pierce.
Functional Pearl: Holey Generators!, May 2022.
Draft.
[ bib ]
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala,
Benjamin C. Pierce, and Steve Zdancewic.
C4: Verified Transactional Objects.
Proc. ACM Program. Lang., 6(OOPSLA1), apr 2022.
[ bib |
DOI |
http ]
Mohsen Lesani, Li-Yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala,
Benjamin C. Pierce, and Steve Zdancewic.
C4: Verified Transactional Objects.
Proc. ACM Program. Lang., 6(OOPSLA1), apr 2022.
[ bib |
DOI |
http ]
Mohsen Lesani, Li-Yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala,
Benjamin C. Pierce, and Steve Zdancewic.
Modular Mechanized Verification of Transactional Predication.
Proc. ACM Program. Lang., 6(OOPSLA1), April 2022.
OOPSLA 2022.
[ bib ]
Mohsen Lesani, Li-Yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala,
Benjamin C. Pierce, and Steve Zdancewic.
C4: Verified Transactional Objects.
Proceedings of the ACM on Programming Languages, OOPSLA, 2022.
[ bib |
.pdf ]
George Tolkachev, Stephen Mell, Steve Zdancewic, and Osbert Bastani.
Counterfactual Explanations for Natural Language Interfaces.
In 60th Annual Meeting of the Association for Computational
Linguistics (ACL), 2022.
(short paper).
[ bib |
.pdf ]
Irene Yoon, Yannick Zakowski, and Steve Zdancewic.
Formal Reasoning About Layered Monadic Interpreters.
Proceedings of the ACM on Programming Languages, 6(ICFP), 2022.
[ bib |
.pdf ]
Stephen Mell, Osbert Bastani, and Steve Zdancewic.
Ideograph: A Language for Expressing and Manipulating Structured
Data.
In Proceedings Twelfth International Workshop on Computing with
Terms and Graphs (TERMGRAPH 2022), pages 65–84. Electronic Proceedings in
Theoretical Computer Science, 2022.
[ bib |
.pdf ]
Pritam Choudhury, Harley Eades III, and Stephanie Weirich.
A Dependent Dependency Calculus.
In Ilya Sergey, editor, Programming Languages and Systems, ESOP
2022, volume 13240 of Lecture Notes in Computer Science, pages
403–430, Cham, 2022. Springer International Publishing.
Artifact available.
[ bib |
DOI |
http ]
Pritam Choudhury, Harley Eades III, and Stephanie Weirich.
Artifact Associated with A Dependent Dependency Calculus.
Technical report, January 2022.
Awarded “Reusable” and “Available” badges by ESOP 2022 Artifact
Evaluation Committee.
[ bib |
DOI ]
Li-Yao Xia.
Executable Semantics with Interaction Trees.
PhD thesis, University of Pennsylvania, 2022.
[ bib |
http ]
Yishuai Li.
Testing By Dualization.
PhD thesis, University of Pennsylvania, 2022.
[ bib |
http ]
Matthew J. Bietz, Nitesh Goyal, Nicole Immorlica, Blair MacIntyre, Andrés
Monroy-Hernández, Benjamin C. Pierce, Sean Rintel, and Donghee Yvette
Wohn.
Social Presence in Virtual Event Spaces.
In CHI Conference on Human Factors in Computing Systems Extended
Abstracts, CHI EA ’22, New York, NY, USA, 2022. Association for Computing
Machinery.
[ bib |
DOI |
http ]
Harrison Goldstein and Benjamin C. Pierce.
Parsing Randomness.
Proc. ACM Program. Lang., (OOPSLA), 2022.
[ bib ]
Harrison Goldstein and Benjamin C. Pierce.
Making Better Choices: Guiding Random Generators with
Derivatives, 2022.
Draft.
[ bib ]
Derek Dreyer and Benjamin C. Pierce.
On being a PhD student of Robert Harper.
Journal of Functional Programming, 32.32, 2022.
[ bib ]
Harrison Goldstein and Benjamin C. Pierce.
Parsing Randomness: Unifying and Differentiating Parsers and
Random Generators.
CoRR, abs/2203.00652, 2022.
[ bib |
DOI |
arXiv |
http ]
Matthew J. Bietz, Nitesh Goyal, Nicole Immorlica, Blair MacIntyre, Andrés
Monroy-Hernández, Benjamin C. Pierce, Sean Rintel, and Donghee Yvette
Wohn.
Social Presence in Virtual Event Spaces.
In Simone D. J. Barbosa, Cliff Lampe, Caroline Appert, and David A.
Shamma, editors, CHI ’22: CHI Conference on Human Factors in
Computing Systems, New Orleans, LA, USA, 29 April 2022 - 5 May 2022, Extended
Abstracts, pages 106:1–106:5. ACM, 2022.
[ bib |
DOI |
http ]
Yao Li, Li-yao Xia, and Stephanie Weirich.
Reasoning about the garden of forking paths.
Proc. ACM Program. Lang., 5(ICFP), August 2021.
[ bib |
DOI |
.pdf ]
Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee.
An Existential Crisis Resolved: Type inference for first-class
existential types.Proc. ACM Program. Lang., 5(ICFP), August 2021.
Distinguished Paper Award.
[ bib |
DOI |
.pdf ]
Yao Li, Li yao Xia, and Stephanie Weirich.
Reasoning about the garden of forking paths (artifact).
Technical report, May 2021.
Awarded “Functional” and “Available” badges by ICFP 2021 Artifact
Evaluation Committee.
[ bib |
DOI ]
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John
Wiegley, Joshua Cohen, and Stephanie Weirich.
Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell
Code.
Journal of Functional Programming, 31:1–40, February 2021.
[ bib |
DOI |
.pdf ]
Lucas Silver and Steve Zdancewic.
Dijkstra Monads Forever: Termination-Sensitive Specifications
for Interaction Trees.
Proceedings of the ACM on Programming Languages, 5(POPL),
January 2021.
[ bib |
.pdf ]
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia,
Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic.
Verifying an HTTP Key-Value Server with Interaction Trees and
VST.
In Liron Cohen and Cezary Kaliszyk, editors, 12th International
Conference on Interactive Theorem Proving (ITP 2021), volume 193 of
Leibniz International Proceedings in Informatics (LIPIcs), pages
32:1–32:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum
für Informatik.
[ bib |
DOI |
http |
.pdf ]
Yishuai Li, Benjamin Pierce, and Steve Zdancewic.
Model-Based Testing of Networked Applications.
In The ACM SIGSOFT International Symposium on Software Testing
and Analysis (ISSTA), 2021.
[ bib ]
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilya Zaichuk, Vadim Zaliva, and
Steve Zdancewic.
Modular, Compositional, and Executable Formal Semantics for LLVM
IR.
Proceedings of the ACM on Programming Languages, 5(ICFP), 2021.
[ bib |
.pdf ]
Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl
Smeltzer, Andrei Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew
Yacavone, and Steve Zdancewic.
A Type System for Extracting Functional Specifications from
Memory-Safe Imperative Programs.
Proceedings of the ACM on Programming Languages, OOPSLA, 2021.
[ bib |
.pdf ]
Pritam Choudhury, Harley D. Eades III, Richard A. Eisenberg, and Stephanie
Weirich.
A Graded Dependent Type System with a Usage-Aware Semantics.
Proc. ACM Program. Lang., 5(POPL), January 2021.
Artifact available.
[ bib |
DOI |
http ]
Stephanie Weirich and Benjamin Pierce.
ICFP 2020 Post-Conference Report, 2021.
[ bib |
arXiv |
http ]
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao
Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, and Steve
Zdancewic.
Verifying an HTTP Key-Value Server with Interaction Trees and
VST.
In Liron Cohen and Cezary Kaliszyk, editors, 12th International
Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1,
2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages
32:1–32:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
[ bib |
DOI |
http ]
Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce,
and Andrew Tolmach.
Security Properties for Stack Safety.
CoRR, abs/2105.00417, 2021.
[ bib |
arXiv |
http ]
Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce,
and Andrew Tolmach.
Security Properties for Stack Safety.
In Workshop on Foundations of Computer Security (FCS), 2021.
[ bib ]
Harrison Goldstein, John Hughes, Leonidas Lampropoulos, and Benjamin C. Pierce.
Do Judge a Test by its Cover: Combining Combinatorial and
Property-Based Testing.
In Nobuko Yoshida, editor, Programming Languages and Systems,
30th European Symposium on Programming, ESOP 2021, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS 2021,
Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume
12648 of Lecture Notes in Computer Science, pages 264–291. Springer,
2021.
[ bib |
DOI |
http ]
Yishuai Li, Benjamin C. Pierce, and Steve Zdancewic.
Model-based testing of networked applications.
In Cristian Cadar and Xiangyu Zhang, editors, ISSTA ’21: 30th
ACM SIGSOFT International Symposium on Software Testing and Analysis,
Virtual Event, Denmark, July 11-17, 2021, pages 529–539. ACM, 2021.
[ bib |
DOI |
http ]
Stephanie Weirich and Benjamin C. Pierce.
ICFP 2020 Post-Conference Report.
CoRR, abs/2104.01239, 2021.
[ bib |
arXiv |
http ]
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie
Weirich.
Artifact for “A Graded Dependent Type System with a Usage-Aware
Semantics”.
Technical report, December 2020.
Awarded “Reusable”, “Functional” and “Available” badges by POPL
2021 Artifact Evaluation Committee.
[ bib |
DOI ]
Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich.
Eta-equivalence in Core Dependent Haskell.
In Marc Bezem and Assia Mahboubi, editors, Post-proceedings of
the 25th International Conference on Types for Proofs and Programs (TYPES
2019), volume 175 of Leibniz International Proceedings in Informatics,
pages 7:1–7:32, Dagstuhl, Germany, sep 2020. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik.
[ bib |
DOI |
http ]
Crista Videira Lopes, Jeanna Matthews, and Benjamin Pierce.
Best Practices for Planning Virtual Conferences, May 2020.
Northstar Meetings Group blog,
https://www.northstarmeetingsgroup.com/Planning-Tips-and-Trends/Event-Planning/Event-Technology/Navigating-New-World-Virtual-Digital-Conferences-in-COVID19-ACM.
[ bib ]
ACM Presidential Task Force on What Conferences Can Do to Replace Face to Face
Meetings (co-chairs, Crista Lopes and Jeanna Matthews; executive editor,
Benjamin C. Pierce).
Virtual Conferences: A Guide to Best Practices, May 2020.
https://www.acm.org/virtual-conferences.
[ bib ]
Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic.
An Equational Theory for Weak Bisimulation via Generalized
Parameterized Coinduction.
In Proceedings of the 9th ACM SIGPLAN International Conference
on Certified Programs and Proofs (CPP), January 2020.
[ bib |
.pdf ]
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha,
Benjamin C. Pierce, and Steve Zdancewic.
Interaction Trees.
Proceedings of the ACM on Programming Languages, 4(POPL),
January 2020.
[ bib |
.pdf ]
Nick Rioux and Steve Zdancewic.
Computation Focusing.
Proceedings of the ACM on Programming Languages, 5(ICFP), 2020.
[ bib |
.pdf ]
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth.
Testing Differential Privacy with Dual Interpreters.
Proc. ACM Program. Lang., 4(OOPSLA):165:1–165:26, 2020.
Selected for a Distinguished Artifact Award.
[ bib |
DOI |
http ]
Benjamin C. Pierce, Michael Hicks, Crista Lopes, and Jens Palsberg.
Conferences in an era of expensive carbon.
Commun. ACM, 63(3):35–37, 2020.
[ bib |
DOI |
http ]
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha,
Benjamin C. Pierce, and Steve Zdancewic.
Interaction trees: representing recursive and impure programs in
Coq.
Proc. ACM Program. Lang., 4(POPL):51:1–51:32, 2020.
Distinguished paper award.
[ bib |
DOI |
http ]
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth.
Testing Differential Privacy with Dual Interpreters.
Proc. ACM Program. Lang., (OOPSLA), 2020.
[ bib ]
Benjamin C. Pierce.
POPLmark 15 Year Retrospective Panel at Certified Programs
and Proofs, 2020.
Written up in
https://blog.sigplan.org/2020/01/29/mechanized-proofs-for-pl-past-present-and-future/.
[ bib |
http ]
Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John
Hughes, Benjamin C. Pierce, and Li-yao Xia.
Beginner’s Luck: A Language for Random Generators.
In Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, editors,
Foundations of Programming and Software systems: Probabilistic
Programming. 2020.
An earlier version appeared in ACM SIGPLAN Symposium on Principles of
Programming Languages (POPL), Jan 2017.
[ bib |
http ]
Antal Spector-Zabusky, Joachim Breitner, Yao Li, and Stephanie Weirich.
Embracing a mechanized formalization gap, October 2019.
[ bib |
arXiv ]
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg.
Replication Package for Article: A Role for Dependent Types in
Haskell.
Technical report, July 2019.
Awarded “Functional” and “Available” badges by ICFP 2019 Artifact
Evaluation Committee.
[ bib |
DOI ]
Benjamin C. Pierce.
The Science of Deep Specification, June 2019.
Opening talk at DeepSpec workshop.
[ bib |
slides ]
Nicolas Koh, Yao Li, Yishuai Li, Li yao Xia, Lennart Beringer, Wolf Honoré,
William Mansky, Benjamin C. Pierce, and Steve Zdancewic.
From C to Interaction Trees: Specifying, Verifying, and Testing
a Networked Server.
In Proceedings of the 8th ACM SIGPLAN International Conference
on Certified Programs and Proofs (CPP), January 2019.
[ bib |
.pdf ]
Marcella Hastings, Brett Hemenway, Daniel Noble, and Steve Zdancewic.
SoK: General Purpose Compilers for Secure Multi-Party
Computation.
In IEEE 2019 Symposium on Security and Privacy (Oakland),
2019.
[ bib |
.pdf ]
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David
Walker, and Steve Zdancewic.
Synthesizing Symmetric Lenses.
Proceedings of the ACM on Programming Languages, 3(ICFP), 2019.
[ bib |
.pdf ]
Jennifer Paykin and Steve Zdancewic.
A HoTT Quantum Equational Theory.
In The 16th International Conference on Quantum Physics and
Logic (QPL), 2019.
extended version available on arXiv.
[ bib |
http ]
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg.
A Role for Dependent Types in Haskell.
Proc. ACM Program. Lang., 3(ICFP), 2019.
[ bib |
DOI |
.pdf ]
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth.
Fuzzi: a three-level logic for differential privacy.
Proc. ACM Program. Lang., 3(ICFP):93:1–93:28, 2019.
[ bib |
DOI |
http ]
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David
Walker, and Steve Zdancewic.
Synthesizing symmetric lenses.
Proc. ACM Program. Lang., 3(ICFP):95:1–95:28, 2019.
[ bib |
DOI |
http ]
Leonidas Lampropoulos, Michael Hicks, and Benjamin C. Pierce.
Coverage guided, property based testing.
Proc. ACM Program. Lang., 3(OOPSLA):181:1–181:29, 2019.
[ bib |
DOI |
http ]
Nicolas Koh, Yao Li, Yishuai Li, Li yao Xia, Lennart Beringer, Wolf Honore,
William Mansky, Benjamin C. Pierce, and Steve Zdancewic.
From C to Interaction Trees: Specifying, Verifying, and
Testing a Networked Server.
In 8th ACM SIGPLAN International Conference on Certified
Programs and Proofs, January 2019.
[ bib |
short version ]
Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David
Walker, and Steve Zdancewic.
Synthesizing Quotient Lenses.
Proceedings of the ACM on Programming Languages (PACMPL ICFP),
September 2018.
[ bib |
short version ]
Michael W. Hicks, Crista Lopes, Jens Palsberg, and Benjamin C. Pierce.
SIGPLAN and Climate Change: A report from the SIGPLAN
committee on climate change, September 2018.
[ bib |
slides ]
Leonidas Lampropoulos and Benjamin C. Pierce.
QuickChick: Property-Based Testing in Coq.
Software Foundations series, volume 4. Electronic textbook, August
2018.
http://www.cis.upenn.edu/ bcpierce/sf.
[ bib ]
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John
Wiegley, and Stephanie Weirich.
Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell
Code (Experience Report).
Proc. ACM Program. Lang., 2(ICFP):89:1–89:16, July 2018.
Artifact Available.
[ bib |
DOI |
http ]
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John
Wiegley, Joshua Cohen, and Stephanie Weirich.
The hs-to-coq tool with examples.
Technical report, July 2018.
Awarded “Artifacts Available” and “Artifacts Evaluated -
Functional” badges by ICFP 2018 Artifact Evaluation Committee.
[ bib |
DOI ]
Benjamin C. Pierce.
In Memoriam Martin Hofmann, July 2018.
The Apple Keynote version includes the music from the presentation,
plus the full text in the presenter notes.
[ bib |
slides ]
Richard Kim and Benjamin C. Pierce.
Carbon Offsets: An Overview for Scientific Societies, June
2018.
Version 1.2.
[ bib |
.pdf ]
Michael W. Hicks, Crista Lopes, Jens Palsberg, and Benjamin C. Pierce.
SIGPLAN and Climate Change: A report from SIGPLAN’s ad hoc
committee on climate change, June 2018.
[ bib |
slides ]
Michael W. Hicks, Crista Lopes, and Benjamin C. Pierce.
Engaging with Climate Change: Some Possible Steps for SIGPLAN
(Preliminary Report of the SIGPLAN Climate Committee, Version 1.2), June
2018.
[ bib |
.pdf ]
Benjamin C. Pierce.
Specifying the DeepSpec Web Server, June 2018.
Talk at DeepSpec workshop.
[ bib |
slides ]
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco
Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg,
Andrew Tolmach, and Brent Yorgey.
Programming Language Foundations.
Software Foundations series, volume 2. Electronic textbook, May 2018.
Version 5.5. http://www.cis.upenn.edu/ bcpierce/sf.
[ bib ]
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco
Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg,
and Brent Yorgey.
Logical Foundations.
Software Foundations series, volume 1. Electronic textbook, May 2018.
Version 5.5. http://www.cis.upenn.edu/ bcpierce/sf.
[ bib ]
Benjamin C. Pierce.
The Science of Deep Specification, April 2018.
Invited keynote at ETAPS / POST.
[ bib |
slides ]
Dmitri Garbuzov, William Mansky, Christine Rizkallah, and Steve Zdancewic.
Structural Operational Semantics for Control Flow Graph
Machines, 2018.
[ bib |
arXiv |
http ]
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve
Zdancewic.
Synthesizing Bijective Lenses.
Proceedings of the ACM on Programming Languages, 2(POPL),
January 2018.
[ bib |
.pdf ]
Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David
Walker, and Steve Zdancewic.
Synthesizing Quotient Lenses.
Proceedings of the ACM on Programming Languages, 2(ICFP), 2018.
[ bib |
.pdf ]
Christine Rizkallah, Dmitri Garbuzov, and Steve Zdancewic.
A Formal Equational Theory for Call-By-Push-Value.
In 9th International Conference on Interactive Theorem Proving
(ITP), 2018.
[ bib |
.pdf ]
Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic.
REQUIRE: Reasoning about Reversible Quantum Circuits.
In The 15th International Conference on Quantum Physics and
Logic (QPL), 2018.
[ bib |
.pdf ]
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie
Weirich.
Total Haskell is Reasonable Coq.
In Proceedings of 7th ACM SIGPLAN International Conference on
Certified Programs and Proofs (CPP’18). ACM, 2018.
New York, NY, USA.
[ bib |
DOI |
http ]
Anastasiya Kravchuk-Kirilyuk Stephanie Weirich, Antoine Voizard.
Locally Nameless at Scale.
The Fourth International Workshop on Coq for Programming Languages,
January 2018.
[ bib |
.pdf ]
Arthur Azevedo de Amorim, Catalin Hritcu, and Benjamin C. Pierce.
The Meaning of Memory Safety.
In Lujo Bauer and Ralf Küsters, editors, Principles of
Security and Trust - 7th International Conference, POST 2018, Held as Part
of the European Joint Conferences on Theory and Practice of Software, ETAPS
2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10804 of
Lecture Notes in Computer Science, pages 79–105. Springer, 2018.
[ bib |
DOI |
http ]
Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans,
Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C Pierce, Marco
Stronati, and Andrew Tolmach.
When good components go bad: Formally secure compilation despite
dynamic compromise.
In Proceedings of the 2018 ACM SIGSAC Conference on Computer and
Communications Security, pages 1351–1368. ACM, 2018.
[ bib ]
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce.
Generating good generators for inductive relations.
PACMPL, 2(POPL):45:1–45:30, 2018.
[ bib |
DOI |
short version |
http ]
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve
Zdancewic.
Synthesizing bijective lenses.
PACMPL, 2(POPL):1:1–1:30, 2018.
[ bib |
DOI |
short version |
http ]
Arthur Azevedo de Amorim, Catalin Hritcu, and Benjamin C. Pierce.
The Meaning of Memory Safety.
In Lujo Bauer and Ralf Küsters, editors, Principles of
Security and Trust - 7th International Conference, POST 2018, Held as Part
of the European Joint Conferences on Theory and Practice of Software, ETAPS
2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10804 of
Lecture Notes in Computer Science, pages 79–105. Springer, 2018.
[ bib |
DOI |
http ]
Benjamin C. Pierce.
The Curse of Knowledge, January 2018.
Talk at Programming Languages Mentoring Workshop (PLMW).
[ bib ]
Jean Yang.
People of Programming Languages: Interview with Benjamin
Pierce, December 2017.
[ bib |
.html ]
Benjamin C. Pierce.
The Science of Deep Specification, September 2017.
WATCH lecture at NSF.
[ bib ]
Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and
Richard A. Eisenberg.
A Specification for Dependent Types in Haskell.
Proc. ACM Program. Lang., 1(ICFP):31:1–31:29, August 2017.
Artifact evaluated as “Available” and Reusable”.
[ bib |
DOI |
http ]
Jennifer Paykin, Robert Rand, and Steve Zdancewic.
QWire: A Core Language for Quantum Circuits.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2017.
[ bib |
.pdf ]
William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti.
Verifying Dynamic Race Detection.
In The 6th ACM SIGPLAN Conference on Certified Programs and
Proofs (CPP 2017), 2017.
[ bib |
.pdf ]
Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong
Shao, Stephanie Weirich, and Steve Zdancewic.
Position paper: The Science of Deep Specification.
Philosophical Transactions of the Royal Society of London A:
Mathematical, Physical and Engineering Sciences, 375(2104), 2017.
[ bib |
DOI |
http ]
Robert Rand, Jennifer Paykin, and Steve Zdancewic.
Qwire Practice: Formal Verification of
Quantum Circuits in Coq.
In The 14th International Conference on Quantum Physics and
Logic (QPL), 2017.
[ bib |
.pdf ]
Jennifer Paykin and Steve Zdancewic.
The Linearity Monad.
In Proceedings of the 10th ACM SIGPLAN International Haskell
Symposium, 2017.
[ bib |
.pdf ]
Stephanie Weirich.
The Influence of Dependent Types, January 2017.
Invited keynote given at POPL 2017.
[ bib ]
Arthur Azevedo de Amorim, Ikram Cherigui, Marco Gaboardi, Justin Hsu, and
Shin-ya Katsumata.
A semantic account of metric preservation.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Paris, France, 2017.
[ bib |
.pdf ]
Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
Coupling proofs are probabilistic product programs.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Paris, France, 2017.
[ bib |
http ]
Arthur Azevedo de Amorim, Cătălin Hriţcu, and Benjamin C. Pierce.
The Meaning of Memory Safety.
In ACM Conference on Computer and Communications Security
(CCS), 2017.
Under submission.
[ bib ]
Benjamin C. Pierce.
The Curse of Knowledge, January 2017.
Talk at Programming Languages Mentoring Workshop (PLMW).
[ bib |
slides ]
Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John
Hughes, Benjamin C. Pierce, and Li-yao Xia.
Beginner’s Luck: A Language for Random Generators.
In 44th ACM SIGPLAN Symposium on Principles of Programming
Languages (POPL), January 2017.
[ bib |
http ]
Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce.
A framework for adaptive differential privacy.
PACMPL, 1(ICFP):10:1–10:29, 2017.
[ bib |
DOI |
http ]
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco
Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg,
and Brent Yorgey.
Software Foundations.
Electronic textbook, 2017.
Version 5.0. http://www.cis.upenn.edu/ bcpierce/sf.
[ bib ]
Benjamin C. Pierce.
Interview with Markus Völter on The Science of Deep
Specification for Omega Tau podcast, November 2016.
[ bib ]
Benjamin C. Pierce.
Interview with Tijs van der Storm on The Science of Deep
Specification for release.nl magazine, November 2016.
[ bib ]
Benjamin C. Pierce.
The Science of Deep Specification, November 2016.
Invited keynote at SPLASH / OOPSLA.
[ bib |
slides ]
Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, Boris
Eng, and Benjamin C. Pierce.
Beyond Good and Evil: Formalizing the Security Guarantees of
Compartmentalizing Compilation.
In 29th IEEE Symposium on Computer Security Foundations (CSF).
IEEE Computer Society Press, July 2016.
arXiv:1602.04503.
[ bib |
http ]
Benjamin C. Pierce.
The Science of Deep Specification, May 2016.
High-Confidence Software Systems (HCSS).
[ bib |
slides ]
Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed.
Visible Type Application.
In European Symposium on Programming (ESOP), pages 229–254,
April 2016.
[ bib |
DOI |
.pdf ]
Steven Keuchel, Stephanie Weirich, and Thomas Tom Schrijvers.
Needle and Knot: Binder Boilerplate Tied Up.
In European Symposium on Programming (ESOP), pages 419–445,
April 2016.
[ bib |
DOI ]
John Hughes, Benjamin C. Pierce, Thomas Arts, and Ulf Norell.
Mysteries of Dropbox: Property-Based Testing of a
Distributed Synchronization Service.
In International Conference on Software Testing, Verification
and Validation (ICST), April 2016.
[ bib |
short version |
slides ]
Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic.
Example-Directed Synthesis: A Type-Theoretic Interpretation.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2016.
[ bib |
.pdf ]
Jennifer Paykin and Steve Zdancewic.
Linear λμ is CP (more or less).
In A List of Successes to Change the World (Wadlerfest), 2016.
[ bib |
.pdf ]
Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios
Vytiniotis.
A Reflection on Types.
In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella,
editors, WadlerFest 2016: A list of successes that can change the
world, LNCS, pages 292–317. Springer, 2016.
[ bib |
DOI |
.pdf ]
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe zero-cost coercions for Haskell.
Journal of Functional Programming, 26, 2016.
[ bib |
DOI |
http |
.pdf ]
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and
Pierre-Yves Strub.
Proving differential privacy via probabilistic couplings.
In IEEE Symposium on Logic in Computer Science
(LICS), New York, New York, 2016.
[ bib |
slides |
http ]
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and
Pierre-Yves Strub.
A program logic for union bounds.
In International Colloquium on Automata, Languages and
Programming (ICALP), Rome, Italy, volume 55 of Leibniz International
Proceedings in Informatics, pages 107:1–107:15. Schloss Dagstuhl–Leibniz
Center for Informatics, 2016.
[ bib |
http ]
Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu.
Synthesizing probabilistic invariants via Doob’s
decomposition.
In International Conference on Computer Aided Verification
(CAV), Toronto, Ontario, volume 9779 of Lecture Notes in Computer
Science, pages 43–61. Springer-Verlag, 2016.
[ bib |
http ]
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús
Gallego Arias, Andy Gordon, Justin Hsu, and Pierre-Yves Strub.
Differentially private Bayesian programming.
In ACM SIGSAC Conference on Computer and Communications
Security (CCS), Vienna, Austria, 2016.
[ bib |
http ]
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin
Hsu, and Pierre-Yves Strub.
Advanced probabilistic couplings for differential privacy.
In ACM SIGSAC Conference on Computer and Communications
Security (CCS), Vienna, Austria, 2016.
[ bib |
http ]
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu,
Aaron Roth, and Pierre-Yves Strub.
Computer-aided verification in mechanism design.
In Conference on Web and Internet Economics (WINE),
Montréal, Québec, 2016.
[ bib |
http ]
Jennifer Paykin, Antal Spector-Zabusky, and Kenneth Foner.
Choose Your Own Derivative (Extended Abstract).
In Proceedings of the 1st International Workshop on Type-Driven
Development, TyDe 2016, pages 58–59, 2016.
[ bib |
DOI ]
Daniel Schoepe, Musard Balliu, Benjamin C. Pierce, and Andrei Sabelfeld.
Explicit Secrecy: A Policy for Taint Tracking.
In IEEE European Symposium on Security and Privacy, EuroS&P
2016, Saarbrücken, Germany, March 21-24, 2016, pages 15–30. IEEE,
2016.
[ bib |
DOI |
http ]
Stephen Chong, Joshua Guttman, Anupam Datta, Andrew C. Myers, Benjamin Pierce,
Patrick Schaumont, Tim Sherwood, and Nickolai Zeldovich.
Report on the NSF Workshop on Formal Methods for Security.
CoRR, abs/1608.00678, 2016.
[ bib |
http ]
Stephen Chong, Joshua Guttman, Anupam Datta, Andrew C. Myers, Benjamin Pierce,
Patrick Schaumont, Tim Sherwood, and Nickolai Zeldovich.
Report on the NSF Workshop on Formal Methods for Security.
CoRR, abs/1608.00678, 2016.
[ bib |
http ]
Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C Pierce.
Programming language techniques for differential privacy.
ACM SIGLOG News, 3(1):34–53, January 2016.
[ bib |
.pdf ]
Benjamin C. Pierce.
A Deep Specification for Dropbox, November 2015.
Keynote address at Clojure/conj.
[ bib |
slides ]
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin
Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach.
Micro-Policies: Formally Verified, Tag-Based Security Monitors.
In 36th IEEE Symposium on Security and Privacy (Oakland S&P).
IEEE, May 2015.
[ bib |
short version |
slides ]
Benjamin C. Pierce.
The Age of Deep Specification, May 2015.
Honorary doctorate address at Chalmers University.
[ bib |
slides ]
Peter-Michael Osera and Steve Zdancewic.
Type-and-Example-Directed Program Synthesis.
In Proc. 2015 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2015.
[ bib |
.pdf ]
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic,
and Viktor Vafeiadis.
A Formal C Memory Model Supporting Integer-Pointer Casts.
In Proc. 2015 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2015.
[ bib |
.pdf ]
William Mansky, Dmitri Garbuzov, and Steve Zdancewic.
An Axiomatic Specification for Sequential Memory Models.
In Computer Aided Verification - 27th International Conference,
CAV 2015, 2015.
[ bib |
.pdf ]
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Everything You Want to Know About Pointer-Based Checking.
In 1st Summit on Advances in Programming Languages, SNAPL
2015, May 3-6, 2015, Asilomar, California, USA, pages 190–208, 2015.
[ bib |
DOI |
http |
.pdf ]
Neelakantan R. Krishnaswami, Jennifer Paykin, and Steve Zdancewic.
Curry-Howard for GUIs.
In POPL Off the Beaten Track (OBT), 2015.
[ bib |
.pdf ]
Robert Rand and Steve Zdancewic.
VPHL: A Verified Partial-Correctness Logic for Probabilistic
Programs.
In Mathematical Foundations of Program Semantics (MFPS), 2015.
[ bib |
.pdf ]
Vilhelm Sjöberg and Stephanie Weirich.
Programming up to Congruence.
In POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 369–382, Mumbai, India, January 2015.
Artifact Evaluated.
[ bib |
DOI |
.pdf ]
Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, and Insup Lee.
Verified ROS-Based Deployment of Platform-Independent Control
Systems.
In Seventh NASA Formal Methods Symposium, pages 248–262,
Pasadena, CA, 2015.
[ bib |
http ]
Justin Hsu.
Death, taxes, and formal verification (Abstract).
In Summit on Advances in Programming Languages (SNAPL),
Asilomar, California, 2015.
[ bib |
slides |
.pdf ]
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu,
Aaron Roth, and Pierre-Yves Strub.
Higher-order approximate relational refinement types for
mechanism design and differential privacy.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Mumbai, India, pages 55–68, 2015.
[ bib |
slides |
http ]
Marco Gaboardi and Justin Hsu.
A Theory AB toolbox.
In Summit on Advances in Programming Languages (SNAPL),
Asilomar, California, volume 32 of Leibniz International Proceedings in
Informatics, pages 129–139. Schloss Dagstuhl–Leibniz Center for
Informatics, 2015.
[ bib |
slides |
.pdf ]
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo
Stefanesco, and Pierre-Yves Strub.
Relational reasoning via probabilistic coupling.
In International Conference on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR), Suva, Fiji, volume 9450 of Lecture
Notes in Computer Science, pages 387–401. Springer-Verlag, 2015.
[ bib |
slides |
http ]
Udit Dhawan, Cătălin Hriţcu, Rafi Rubin, Nikos Vasilakis, Silviu
Chiricescu, Jonathan M. Smith, Thomas F. Knight, Jr., Benjamin C. Pierce,
and André DeHon.
Architectural Support for Software-Defined Metadata Processing,
2015.
[ bib |
.html ]
Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas
Lampropoulos, and Benjamin C. Pierce.
Foundational Property-Based Testing.
In International Conference on Interactive Theorem Proving
(ITP), 2015.
[ bib ]
Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner.
Symmetric Lenses.
Journal of the ACM, 2015.
To appear; extended abstract in POPL 2011.
[ bib |
short version ]
Benjamin C. Pierce.
Micro-Policies: A Framework for Tag-Based Security Monitors,
December 2014.
Distinguished Lecture at University of Minnesota.
[ bib |
slides ]
Benjamin C. Pierce.
Mysteries of Dropbox, November 2014.
Keynote address at CERN Workshop on Cloud Services for File
Synchronisation and Sharing.
[ bib |
slides ]
Benjamin C. Pierce.
Interview with Luke Muehlhauser on Clean-Slate Security
Architectures for Machine Intelligence Research Institute blog, May 2014.
[ bib ]
Benjamin C. Pierce.
Programmable Hardware Support for Ubiquitous Micro-Policy
Enforcement, May 2014.
Talk at High-Confidence Software Systems.
[ bib |
slides ]
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
WatchdogLite: Hardware-Accelerated Compiler-Based Pointer
Checking.
In Proceedings of Annual IEEE/ACM International Symposium on
Code Generation and Optimization, CGO ’14, pages 175:175–175:184. ACM,
2014.
[ bib |
DOI |
http |
.pdf ]
Jennifer Paykin and Steve Zdancewic.
A Linear/Producer/Consumer model of Classical Linear Logic.
Technical report, University of Pennsylvania, 2014.
[ bib |
.pdf ]
Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic.
A Core Quantitative Coeffect Calculus.
In Proc. of the 23rd European Symposium on Programming (ESOP),
volume 8410, pages 351–370, 2014.
[ bib |
.pdf ]
Jennifer Paykin and Steve Zdancewic.
A Linear/Producer/Consumer model of Classical Linear Logic
(extended abstract).
In Third International Workshop on Linearity, LINEARITY, 2014.
[ bib |
.pdf ]
B. Valiron and S. Zdancewic.
Modeling Simply-Typed Lambda Calculi in the Category of Finite
Vector Spaces.
Scientific Annals of Computer Science, 24(2):325–368, 2014.
[ bib |
DOI |
.pdf ]
Benoît Valiron and Steve Zdancewic.
Finite vector spaces as model of simply-typed lambda-calculi.
In Proceedings of the 11th International Colloquium on
Theoretical Aspects of Computing (ICTAC 14), 2014.
[ bib |
.pdf ]
Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Combining Proofs and Programs in a Dependently Typed Language.
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’14, page 33–45, New York, NY,
USA, 2014. Association for Computing Machinery.
[ bib |
DOI |
.pdf ]
Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie
Weirich.
Closed type families with overlapping equations.
In POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 671–683, San Diego, CA, USA, January 2014.
[ bib |
.pdf ]
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe Zero-Cost Coercions for Haskell.
In Proceedings of the 19th ACM SIGPLAN International Conference
on Functional Programming, ICFP ’14, page 189–202, New York, NY, USA,
2014. Association for Computing Machinery.
[ bib |
DOI |
http ]
Stephanie Weirich.
Depending on Types, 2014.
Invited keynote given at ICFP 2014.
[ bib ]
Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan,
Benjamin C. Pierce, and Aaron Roth.
Differential privacy: An economic method for choosing epsilon.
In IEEE Computer Security Foundations Symposium
(CSF), Vienna, Austria, pages 398–410, 2014.
[ bib |
slides |
http ]
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu,
César Kunz, and Pierre-Yves Strub.
Proving differential privacy in Hoare logic.
In IEEE Computer Security Foundations Symposium
(CSF), Vienna, Austria, pages 411–424, 2014.
[ bib |
http ]
Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and
Justin Hsu.
Really natural linear indexed type-checking.
In Symposium on Implementation and Application of Functional
Programming Languages (IFL), Boston, Massachusetts, pages 5:1–5:12. ACM
Press, 2014.
[ bib |
slides |
http ]
Maxime Dénès, Catalin Hritcu, Leonidas Lampropoulos, Zoe Paraskevopoulou,
and Benjamin C. Pierce.
QuickChick: Property-Based Testing for Coq (abstract).
In VSL, 2014.
[ bib |
.html ]
Daniel Wagner.
Symmetric Edit Lenses: A New Foundation for Bidirectional
Languages.
PhD thesis, University of Pennsylvania, 2014.
[ bib |
.pdf ]
Benjamin C. Pierce.
Principles, Meet Practice: An Early Retrospective on SAFE,
January 2014.
Talk at Principles in Practice Workshop (PiP).
[ bib |
slides ]
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange,
Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy
Pollack, and Andrew Tolmach.
A Verified Information-Flow Architecture.
In Proceedings of the 41st Symposium on Principles of
Programming Languages, POPL, January 2014.
Full version in Journal of Computer Security, Special Issue on
Verified Information Flow Security, Dec 2016.
[ bib |
full version |
.pdf ]
Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan,
Benjamin C. Pierce, and Aaron Roth.
Differential Privacy: An Economic Method for Choosing Epsilon.
In Computer Security Foundations Symposium (CSF), 2014.
[ bib |
.pdf ]
Udit Dhawan, Nikos Vasilakis, Raphael Rubin, Silviu Chiricescu, Jonathan M.
Smith, Thomas F. Knight, Benjamin C. Pierce, and André DeHon.
PUMP – A Programmable Unit for Metadata Processing.
In Proceedings of the 3rd International Workshop on Hardware and
Architectural Support for Security and Privacy, HASP ’14, New York, NY, USA,
2014. ACM.
[ bib |
DOI |
http ]
Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie
Weirich.
Closed type families with overlapping equations (Extended
version).
Technical Report MS-CIS-13-10, University of Pennsylvania, November
2013.
[ bib |
http ]
Silviu Chiricescu, André DeHon, Delphine Demange, Suraj Iyer, Aleksey
Kliger, Greg Morrisett, Benjamin C. Pierce, Howard Reubenstein, Jonathan M.
Smith, Gregory T. Sullivan, Arun Thomas, Jesse Tov, Christopher M. White, and
David Wittenberg.
SAFE: A Clean-Slate Architecture for Secure Systems.
In Proceedings of the IEEE International Conference on
Technologies for Homeland Security, November 2013.
[ bib ]
Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Antal
Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and
Leonidas Lampropoulos.
Testing Noninterference, Quickly.
In 18th ACM SIGPLAN International Conference on Functional
Programming (ICFP), September 2013.
Full version in Journal of Functional Programming, special issue for
ICFP 2013, 26:e4 (62 pages), April 2016. Technical Report available as
arXiv:1409.0393.
[ bib |
http ]
Benjamin C. Pierce.
The SAFE Machine: An Architecture for Pervasive Information
Flow, June 2013.
Invited talk at Computer Security Foundations Symposium (CSF).
[ bib |
slides ]
Benoît Montagu, Benjamin C. Pierce, and Randy Pollack.
A Theory of Information-Flow Labels.
In Proceedings of the 2013 IEEE Computer Security Foundations
Symposium, June 2013.
[ bib |
short version ]
Santosh Nagarakatte, Milo M K Martin, and Steve Zdancewic.
Hardware-enforced Comprehensive Memory Safety.
IEEE MICRO’s “Top Picks of Architecture Conferences of 2012”
Issue (Micro Top Picks’2013), May/June 2013.
[ bib |
http ]
Cătălin Hriţcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce,
and Greg Morrisett.
All Your IFCException Are Belong To Us.
In 34th IEEE Symposium on Security and Privacy (Oakland), May
2013.
[ bib |
short version ]
Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner.
Edit languages for information trees.
In Second International Workshop on Bidirectional
Transformations (BX), April 2013.
[ bib ]
Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael
Osera, Milo M.K. Martin, and Steve Zdancewic.
Ironclad C++: A library-Augmented Type-Safe Subset of C++.
Technical Report MS-CIS-13-05, University of Pennsylvania, March
2013.
[ bib |
.pdf ]
Garrin Kimmel, Aaron Stump, Harley D. Eades, Peng Fu, Tim Sheard, Stephanie
Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathin Collins, and Ki Yunh
Anh.
Equational reasoning about programs with general recursion and
call-by-value semantics.
Progress in Informatics, (10):19–48, March 2013.
[ bib |
http ]
Zhengjiang Hu, Shin-Cheng Mu, and Stephanie Weirich.
Guest Editorial: Advanced programming techniques for
construction of robust, generic and evolutionary programs.
Progress in Informatics, (10):1–2, March 2013.
[ bib |
DOI |
http ]
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Formal Verification of SSA-Based Optimizations for LLVM.
In Proc. 2013 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2013.
[ bib |
.pdf ]
Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael
Osera, Milo M. K. Martin, and Steve Zdancewic.
Ironclad C++: A Library-Augmented Type-Safe Subset of C++.
In Proceedings of the 28th Annual ACM SIGPLAN Conference on
Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA),
2013.
[ bib |
.pdf ]
Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam,
Nathan Michael, George J. Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie
Weirich, and Insup Lee.
Towards synthesis of platform-aware attack-resilient control
systems: extended abstract.
In HiCoNS ’13: Proceedings of the 2nd ACM international
conference on High confidence networked systems, pages 75–76, New York, NY,
USA, 2013.
[ bib ]
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
System FC with Explicit Kind Equality.
In Proceedings of the 18th ACM SIGPLAN International Conference
on Functional Programming, ICFP ’13, page 275–286, New York, NY, USA,
2013. Association for Computing Machinery.
[ bib |
DOI |
http |
.pdf ]
Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, Justin Hsu,
and Benjamin C. Pierce.
Automatic sensitivity analysis using linear dependent types.
In International Workshop on Foundational and Practical Aspects
of Resource Analysis (FOPARA), informal proceedings, 2013.
[ bib |
.pdf ]
Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C.
Pierce.
Linear dependent types for differential privacy.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Rome, Italy, pages 357–370, 2013.
[ bib |
http ]
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
System FC with explicit kind equality.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), Boston, Massachusetts, pages 275–286, 2013.
[ bib |
.pdf ]
Stephen Brookes, Benjamin C. Pierce, Gordon D. Plotkin, and Dana S. Scott.
Dedication to John Reynolds.
Electr. Notes Theor. Comput. Sci., 298:3–5, 2013.
Special Issue: Proceedings of the 29th Conference on Mathematical
Foundations of Programming Semantics (MFPS).
[ bib |
DOI |
http ]
Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C.
Pierce.
Linear Dependent Types for Differential Privacy.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Rome, Italy, January 2013.
[ bib |
short version ]
Loris D’Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas
Haeberlen, and Benjamin Pierce.
Sensitivity analysis using type-based constraints.
In Proceedings of the 1st annual workshop on Functional
programming concepts in domain-specific languages, FPCDSL ’13, pages 43–50,
New York, NY, USA, 2013. ACM.
[ bib |
DOI |
http ]
Benjamin C. Pierce.
Differential Privacy in the Programming Languages Community,
October 2012.
Invited tutorial at DIMACS Workshop on Recent Work on
Differential Privacy across Computer Science.
[ bib |
slides ]
Udit Dhawan, Albert Kwon, Edin Kadric, Cătălin Hriţcu, Benjamin C.
Pierce, Jonathan M. Smith, Gregory Malecha, Greg Morrisett, Thomas F.
Knight, Jr., Andrew Sutherland, Tom Hawkins, Amanda Zyxnfryx, David
Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan, and André DeHon.
Hardware Support for Safety Interlocks and Introspection.
In SASO Workshop on Adaptive Host and Network Security,
September 2012.
[ bib |
.pdf ]
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Watchdog: Hardware for Safe and Secure Manual Memory Management
and Full Memory Safety.
In Proceedings of the 39th International Symposium on Computer
Architecture (ISCA), June 2012.
[ bib |
.pdf ]
Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich.
Contracts made manifest.
Journal of Functional Programming, 22(3):225–274, May 2012.
[ bib ]
Stephanie Weirich.
Dependently typed programming in GHC, May 2012.
Invited keynote given at FLOPS 2012.
[ bib |
slides ]
Benjamin C. Pierce.
Linguistic Foundations for Bidirectional Transformations, May
2012.
Invited tutorial at Principles of Database Systems (PODS).
[ bib |
slides ]
Kathleen Fisher, Ronald Garcia, and Stephanie Weirich.
Nourishing the future of the field: the programming language
mentoring workshop 2012, April 2012.
[ bib |
DOI ]
Benjamin C. Pierce.
Types à la Milner, April 2012.
Talk at Philly Emerging Technologies Conference.
[ bib ]
Benjamin C. Pierce.
Types à la Milner, April 2012.
Invited talk at Milner Symposium.
[ bib |
slides ]
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Formalizing the LLVM Intermediate Representation for Verified
Program Transformations.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2012.
[ bib |
.pdf ]
Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic.
Dependent Ineroperability.
In The Sixth ACM SIGPLAN Workshop on Programming Languages meets
Program Verification (PLPV), 2012.
[ bib |
.pdf ]
Jianzhou Zhao and Steve Zdancewic.
Mechanized Verification of Computing Dominators for Formalizing
Compilers.
In The Second International Conference on Certified Programs and
Proofs (CPP), Lecture Notes in Computer Science, pages 27–42, 2012.
[ bib |
.pdf ]
Stephanie Weirich and Chris Casinghino.
Generic Programming with Dependent Types.
In Jeremy Gibbons, editor, Generic and Indexed Programming,
number 7470 in Lecture Notes in Computer Science, pages 217–258.
Springer-Verlag Berlin Heidelberg, 2012.
[ bib |
.pdf ]
Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
Dimitrios Vytiniotis, and José Pedro Magalhaẽs.
Giving Haskell A Promotion.
In Seventh ACM SIGPLAN Workshop on Types in Language Design and
Implementation (TLDI ’12), pages 53–66, 2012.
[ bib |
.pdf ]
Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard,
Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and
Ki Yung Ahn.
Equational Reasoning about Programs with General Recursion and
Call-by-value Semantics.
In Sixth ACM SIGPLAN Workshop Programming Languages meets
Program Verification (PLPV ’12), pages 15–26, 2012.
[ bib |
.pdf ]
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley
D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie
Weirich.
Irrelevance, Heterogenous Equality, and Call-by-value Dependent
Type Systems.
In Fourth workshop on Mathematically Structured Functional
Programming (MSFP ’12), pages 112–162, 2012.
[ bib |
.pdf ]
Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Step-Indexed Normalization for a Language with General
Recursion.
In Fourth workshop on Mathematically Structured Functional
Programming (MSFP ’12), pages 25–39, 2012.
[ bib |
.pdf ]
Umut A. Acar, James Cheney, and Stephanie Weirich.
Editorial - Special issue dedicated to ICFP 2010.
J. Funct. Program., 22(4-5):379–381, 2012.
[ bib |
DOI ]
Benjamin C. Pierce and Stephanie Weirich.
Preface to Special Issue on the POPLMark Challenge.
J. Autom. Reasoning, 49(3):301–302, 2012.
[ bib ]
Benjamin C. Pierce.
Verification Challenges of Pervasive Information Flow, January
2012.
Invited talk at Programming Languages Meets Program
Verification workshop (PLPV).
[ bib |
slides ]
Benjamin C. Pierce.
Types, January 2012.
Invited talk at Programming Languages Mentoring Workshop.
[ bib |
slides ]
Benjamin C. Pierce and editors Stephanie Weirich.
Special Issue on the POPLMark Challenge.
J. Autom. Reasoning, 49(3), 2012.
[ bib ]
Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner.
Edit Lenses.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Philadelphia, Pennsylvania, January
2012.
[ bib |
short version |
slides ]
André DeHon, Ben Karel, Thomas F. Knight, Jr., Gregory Malecha,
Benoît Montagu, Robin Morisset, Greg Morrisett, Benjamin C. Pierce, Randy
Pollack, Sumit Ray, Olin Shivers, Jonathan M. Smith, and Gregory Sullivan.
Preliminary Design of the SAFE Platform.
In 6th Workshop on Programming Languages and Operating Systems,
PLOS, October 2011.
[ bib |
.pdf ]
Andreas Haeberlen, Benjamin C. Pierce, and Arjun Narayan.
Differential Privacy Under Fire.
In Proceedings of the 20th USENIX Security Symposium, August
2011.
[ bib |
.pdf ]
Stephanie Weirich.
Combining Proofs and Programs, June 2011.
Joint invited speaker for Rewriting Techniques and Applications (RTA
2011) and Typed Lambda Calculi and Applications (TLCA 2011).
[ bib |
slides ]
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic.
Generative Type Abstraction and Type-level Computation.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2011.
[ bib |
.pdf ]
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic.
Generative Type Abstraction and Type-level Computation.
In POPL 11: 38th ACM SIGACT-SIGPLAN Symposium on Principles of
Programming Languages, January 26–28, 2011. Austin, TX, USA., pages
227–240, January 2011.
[ bib |
.pdf ]
Stephanie Weirich, Brent A. Yorgey, and Tim Sheard.
Binders Unbound.
In Proceeding of the 16th ACM SIGPLAN International Conference
on Functional Programming, ICFP ’11, pages 333–345, New York, NY, USA,
2011.
[ bib |
.pdf ]
João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C.
Pierce.
Polymorphic Contracts.
In Gilles Barthe, editor, European Symposium on Programming
(ESOP), Saarbrücken, Germany, volume 6602 of Lecture Notes in
Computer Science, pages 18–37. Springer, 2011.
[ bib ]
Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner.
Symmetric Lenses.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Austin, Texas, January 2011.
[ bib |
short version |
full version ]
Tim Sheard, Aaron Stump, and Stephanie Weirich.
Language-Based Verification Will Change The World.
In 2010 FSE/SDP Workshop on the Future of Software Engineering
Research, pages 343–348, November 2010.
Position paper.
[ bib |
.pdf ]
Benjamin C. Pierce.
creativity: sensitivity and surprise, October 2010.
Keynote talk at SPLASH / Onward!
[ bib |
slides ]
Stephanie Weirich, editor.
International Conference on Functional Programming. ACM Press,
September 2010.
[ bib ]
Stephanie Weirich.
ICFP 2010 PC Chair’s Report, September 2010.
[ bib ]
Jason Reed and Benjamin C. Pierce.
Distance Makes the Types Grow Stronger: A Calculus for
Differential Privacy.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), Baltimore, Maryland, September 2010.
[ bib |
short version ]
Davi M. J. Barbosa, Julien Cretin, Nate Foster, Michael Greenberg, and
Benjamin C. Pierce.
Matching Lenses: Alignment and View Update.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), Baltimore, Maryland, September 2010.
[ bib |
tech report |
short version ]
Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich.
Termination Casts: A Flexible Approach to Termination with
General Recursion.
In Workshop on Partiality and Recursion in Interactive Theorem
Provers, pages 76–93, Edinburgh, Scotland, July 2010.
[ bib |
.pdf ]
Benjamin C. Pierce.
Proof Assistant as Teaching Assistant: A View from the
Trenches, July 2010.
Keynote address at International Conference on Interactive
Theorem Proving (ITP).
[ bib |
slides ]
Brian Aydemir and Stephanie Weirich.
LNgen: Tool Support for Locally Nameless Representations, June
2010.
[ bib |
http ]
Aaron Bohannon and Benjamin C. Pierce.
Featherweight Firefox: Formalizing the Core of a Web
Browser.
In Usenix Conference on Web Application Development (WebApps),
June 2010.
[ bib |
short version ]
Jason Reed, Adam J. Aviv, Daniel Wagner, Andreas Haeberlen, Benjamin C. Pierce,
and Jonathan M. Smith.
Differential Privacy for Collaborative Security.
In European Workshop on System Security (EUROSEC), April 2010.
[ bib |
manuscript ]
Dimitrios Vytiniotis and Stephanie Weirich.
Parametricity, Type Equality and Higher-order Polymorphism.
Journal of Functional Programming, 20(2):175–210, March 2010.
[ bib |
.pdf ]
Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic.
Lightweight linear types in System Fo.
In ACM SIGPLAN International Workshop on Types in Languages
Design and Implementation (TLDI), pages 77–88, 2010.
[ bib |
.pdf ]
Peng Li and Steve Zdancewic.
Arrows for Secure Information Flow.
Theoretical Computer Science, 411(19):1974–1994, 2010.
[ bib |
.pdf ]
Karl Mazurak and Steve Zdancewic.
Lolliproc: to Concurrency from Classical Linear Logic via
Curry-Howard and Control.
In Proc. of the 15th ACM SIGPLAN International Conference on
Functional Programming (ICFP), 2010.
[ bib |
.pdf ]
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic.
CETS: Compiler-Enforced Temporal Safety for C.
In Proceedings of the ACM International Symposium on Memory
Management (ISMM), 2010.
[ bib |
.pdf ]
Jianzhou Zhao, Qi Zhang, and Steve Zdancewic.
Relational Parametricity for Polymorphic Linear Lambda Calculus
(Extended TR).
2010.
[ bib |
.pdf ]
Jianzhou Zhao, Qi Zhang, and Steve Zdancewic.
Relational Parametricity for Polymorphic Linear Lambda
Calculus.
In Proceedings of the Eighth ASIAN Symposium on Programming
Languages and Systems (APLAS), 2010.
[ bib |
.pdf ]
Stephanie Weirich and Chris Casinghino.
Arity-generic type-generic programming.
In ACM SIGPLAN Workshop on Programming Languages Meets Program
Verification (PLPV), pages 15–26, January 2010.
[ bib |
.pdf ]
Limin Jia, Jianzhou Zhao, Vilhem Sjöberg, and Stephanie Weirich.
Dependent types and Program Equivalence.
In 37th ACM SIGACT-SIGPLAN Symposium on Principles of
Programming Languages (POPL), pages 275–286, Madrid, Spain, January 2010.
[ bib |
.pdf ]
Benjamin C. Pierce, Alessandro Romanel, and Daniel Wagner.
The Spider Calculus: Computing in Active Graphs, 2010.
Manuscript, available from
http://www.cis.upenn.edu/ bcpierce/papers/spider_calculus.pdf.
[ bib |
manuscript ]
Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich.
Contracts Made Manifest.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Madrid, Spain. ACM, January 2010.
[ bib |
short version ]
Benjamin C. Pierce.
Lambda, The Ultimate TA: Using a Proof Assistant to Teach
Programming Language Foundations, September 2009.
Keynote address at International Conference on Functional
Programming (ICFP).
[ bib |
slides ]
Stephanie Weirich.
Haskell 2009 PC Chair’s Report, August 2009.
[ bib ]
J. Nathan Foster, Benjamin C. Pierce, and Steve Zdancewic.
Updatable Security Views.
In IEEE Computer Security Foundations Symposium (CSF), Port
Jefferson, NY, July 2009.
[ bib |
conference version ]
Benjamin C. Pierce.
Foundations for Bidirectional Programming, or: How To Build a
Bidirectional Programming Language, June 2009.
Keynote address at International Conference on Model
Transformation (ICMT).
[ bib |
slides ]
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic.
SoftBound: Highly Compatible and Complete Spatial Memory
Safety for C.
In Proc. 2009 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2009.
[ bib |
.pdf ]
J. Nathan Foster, Benjamin C. Pierce, and Steve Zdancewic.
Updatable Security Views.
In Proc. of 22nd IEEE Computer Security Foundations Symposium
(CSF), 2009.
[ bib |
.pdf ]
Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and
Steve Zdancewic.
Reactive Noninterference.
In ACM Computer and Communications Security Conference (CCS),
2009.
[ bib |
.pdf ]
Limin Jia and Steve Zdancewic.
Encoding information flow in Aura.
In Proceedings of the 2009 Workshop on Programming Languages and
Analysis for Security (PLAS), pages 17–29, 2009.
[ bib |
.pdf ]
Michael J. May, Carl A. Gunter, Insup Lee, and Steve Zdancewic.
Strong and Weak Policy Relations.
In POLICY 2009, IEEE International Symposium on Policies for
Distributed Systems and Networks, pages 33–36, 2009.
[ bib ]
Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and
Steve Zdancewic.
Reactive Noninterference.
In CCS ’09: Proceedings of the 16th ACM conference on Computer
and communications security, pages 79–90, New York, NY, USA, 2009. ACM.
[ bib |
DOI ]
Benjamin C. Pierce.
POPL 2009 PC Chair’s Report, January 2009.
[ bib |
slides ]
Benjamin C. Pierce, editor.
Principles of Programming Languages (POPL). ACM Press, 2009.
[ bib ]
Véronique Benzaken, Giuseppe Castagna, Haruo Hosoya, Benjamin C. Pierce,
and Stijn Vansummeren.
XML Typechecking.
In Encyclopedia of Database Systems. Springer, 2009.
[ bib ]
Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph
Schorr, and Steve Zdancewic.
AURA: A Programming Language for Authorization and Audit.
In Proc. of the 13th ACM SIGPLAN International Conference on
Functional Programming (ICFP), Victoria, British Columbia, Canada, September
2008.
[ bib |
.pdf ]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.
FPH: First-class polymorphism for Haskell.
In ICFP 2008: The 13th ACM SIGPLAN International Conference on
Functional Programming, pages 295–306, Victoria, BC, Canada, September
2008.
[ bib |
.pdf ]
J. Nathan Foster, Alexandre Pilkiewicz, and Benjamin C. Pierce.
Quotient Lenses.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), Victoria, Canada, September 2008.
[ bib |
short version ]
Benjamin C. Pierce.
Types Considered Harmful, May 2008.
Invited talk at Mathematical Foundations of Programming
Semantics (MFPS).
[ bib |
slides ]
Benjamin C. Pierce.
Using a Proof Assistant to Teach Programming Language
Foundations, or, Lambda, the Ultimate TA, April 2008.
White paper.
[ bib |
short version ]
Joe Devietti, Colin Blundell, Milo M.K. Martin, and Steve Zdancewic.
HardBound: Architectural Support for Spatial Safety of the C
Programming Language.
In International Conference on Architectural Support for
Programming Languages and Operating Systems (ASPLOS), March 2008.
[ bib |
.pdf ]
Stephen Tse and Steve Zdancewic.
Run-time principals in information-flow type systems.
ACM Transactions on Programming Languages and Systems, 30(1):6,
2008.
[ bib |
.pdf ]
Jeffrey C. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic.
Evidence-based Audit, Technical Appendix.
Technical Report MS-CIS-08-09, University of Pennsylvania, 2008.
[ bib |
.pdf ]
Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph
Schorr, and Steve Zdancewic.
AURA:Preliminary Technical Results.
Technical Report MS-CIS-08-10, University of Pennsylvania, 2008.
[ bib |
.pdf ]
Stephen Tse and Steve Zdancewic.
Concise Concrete Syntax.
Technical Report MS-CIS-08-11, University of Pennsylvania, 2008.
[ bib |
.pdf ]
Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic.
Evidence-based Audit.
In Proc. of 21st IEEE Computer Security Foundations Symposium
(CSF), pages 177–191. IEEE Computer Society Press, 2008.
[ bib |
.pdf ]
Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre Pilkiewicz, and
Alan Schmitt.
Boomerang: Resourceful Lenses for String Data.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), San Francisco, California, January 2008.
[ bib |
tech report |
short version ]
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and
Stephanie Weirich.
Engineering formal metatheory.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), San Francisco, California, pages 3–15.
ACM, January 2008.
[ bib |
short version ]
Benjamin C. Pierce.
Adventures in Bi-Directional Programming, December 2007.
FSTTCS invited talk.
[ bib |
slides ]
Sanjeev Khanna, Keshav Kunal, and Benjamin C. Pierce.
A Formal Investigation of Diff3.
In Arvind and Prasad, editors, Foundations of Software
Technology and Theoretical Computer Science (FSTTCS), December 2007.
[ bib |
short version ]
Karl Mazurak and Steve Zdancewic.
ABash: Finding Bugs in Bash Scripts.
In ACM SIGPLAN Workshop on Programming Languages and Analysis
for Security (PLAS), June 2007.
[ bib |
.pdf ]
J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce,
and Alan Schmitt.
Combinators for bidirectional tree transformations: A
linguistic approach to the view-update problem.
ACM Transactions on Programming Languages and Systems,
29(3):17, May 2007.
Preliminary version presented at the Workshop on Programming
Language Technologies for XML (PLAN-X), 2004; extended abstract presented at
Principles of Programming Languages (POPL), 2005.
[ bib |
DOI |
conference version |
full version |
slides ]
Dimitrios Vytiniotis and Stephanie Weirich.
Free theorems and runtime type representations.
In Mathematical Foundations of Programming Semantics (MFPS
XXIII), pages 357–373, New Orleans, LA, USA, April 2007.
[ bib |
.ps |
.pdf ]
Dimitrios Vytiniotis and Stephanie Weirich.
Dependent types: Easy as PIE.
In Marco T. Morazán and Henrik Nilsson, editors, Draft
Proceedings of the 8th Symposium on Trends in Functional Programming, pages
XVII–1—XVII–15. Dept. of Math and Computer Science, Seton Hall
University, April 2007.
TR-SHU-CS-2007-04-1.
[ bib |
.pdf ]
Peng Li and Steve Zdancewic.
Combining Events And Threads For Scalable Network Services.
In Proc. 2007 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), pages 189–199, 2007.
[ bib |
.ps ]
Jeffrey A. Vaughan and Steve Zdancewic.
A Cryptographic Decentralized Label Model.
In IEEE 2007 Symposium on Security and Privacy (Oakland),
pages 192–206, 2007.
[ bib |
.ps |
.pdf ]
Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields.
Practical type inference for arbitrary-rank types.
Journal of Functional Programming, 17(1):1–82, January 2007.
[ bib |
http ]
J. Nathan Foster, Benjamin C. Pierce, and Alan Schmitt.
A Logic Your Typechecker Can Count On: Unordered Tree Types in
Practice.
In Workshop on Programming Language Technologies for XML
(PLAN-X), informal proceedings, January 2007.
[ bib |
conference version |
slides ]
J. Nathan Foster, Michael B. Greenwald, Christian Kirkegaard, Benjamin C.
Pierce, and Alan Schmitt.
Exploiting Schemas in Data Synchronization.
Journal of Computer and System Sciences, 73(4):669–689, 2007.
Extended abstract in Database Programming Languages (DBPL)
2005.
[ bib |
tech report |
short version |
full version |
slides ]
Stephanie Weirich.
Type-Safe Run-time Polytypic Programming.
Journal of Functional Programming, 16(10):681–710, November
2006.
[ bib |
.pdf ]
Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey
Washburn.
Simple unification-based type inference for GADTs.
In International Conference on Functional Programming (ICFP),
pages 50–61, Portland, OR, USA, September 2006.
[ bib |
.pdf ]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Boxy type inference for higher-rank types and impredicativity.
In International Conference on Functional Programming (ICFP),
pages 251–262, Portland, OR, USA, September 2006.
[ bib |
http ]
Geoffrey Washburn and Stephanie Weirich.
Good Advice for Type-directed Programming: Aspect-oriented
Programming and Extensible Generic Functions.
In Workshop on Generic Programming (WGP), pages 33–44,
Portland, OR, USA, September 2006.
[ bib |
.pdf ]
Stephanie Weirich.
RepLib: A library for derivable type classes.
In Haskell Workshop, pages 1–12, Portland, OR, USA, September
2006.
[ bib |
http ]
Andrew J. Kennedy and Benjamin C. Pierce.
On Decidability of Nominal Subtyping with Variance, September
2006.
FOOL-WOOD ’07.
[ bib |
short version ]
Brian Aydemir, Aaron Bohannon, and Stephanie Weirich.
Nominal Reasoning Techniques in Coq.
In International Workshop on Logical Frameworks and
Meta-Languages:Theory and Practice (LFMTP), pages 60–69, Seattle, WA, USA,
August 2006.
[ bib |
.pdf ]
Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Simple unification-based type inference for GADTs, Technical
Appendix.
Technical Report MS-CIS-05-22, University of Pennsylvania, April
2006.
[ bib |
.pdf ]
Benjamin C. Pierce.
The Weird World of Bi-Directional Programming, March 2006.
ETAPS invited talk.
[ bib |
slides ]
Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic.
Enforcing Robust Declassification and Qualified Robustness.
Journal of Computer Security, 14(2):157–196, 2006.
[ bib |
.pdf ]
Jay Ligatti, David Walker, and Steve Zdancewic.
A Type-theoretic Interpretation of Pointcuts and Advice.
Science of Computer Programming: Special Issue on Foundations of
Aspect-Oriented Programming, pages 240–266, 2006.
[ bib |
.pdf ]
Nikhil Swamy, Michael Hicks, Stephen Tse, and Steve Zdancewic.
Managing Policy Updates in Security-Typed Languages.
In Proc. of 19th IEEE Computer Security Foundations Workshop
(CSFW), pages 202–216. IEEE Computer Society Press, 2006.
[ bib |
.pdf ]
Peng Li and Steve Zdancewic.
Encoding Information Flow in Haskell.
In Proc. of 19th IEEE Computer Security Foundations Workshop
(CSFW), pages 16–27. IEEE Computer Society Press, 2006.
[ bib |
.pdf ]
Rajeev Alur, Pavol Černý, and Steve Zdancewic.
Preserving Secrecy under Refinement.
In Proc. of 33rd International Colloquium on Automata, Languages
and Programming (ICALP), pages 107–118, 2006.
[ bib |
.pdf ]
Vladimir Gapeyev, François Garillot, and Benjamin C. Pierce.
Statically Typed Document Transformation: An Xtatic
Experience.
In Workshop on Programming Language Technologies for XML
(PLAN-X), informal proceedings, January 2006.
Available from the Xtatic web site.
[ bib |
tech report |
.pdf ]
Michael B. Greenwald, Sanjeev Khanna, Keshav Kunal, Benjamin C. Pierce, and
Alan Schmitt.
Agreeing to Agree: Conflict Resolution for Optimistically
Replicated Data.
In Shlomi Dolev, editor, International Symposium on Distributed
Computing (DISC), 2006.
[ bib |
tech report |
short version |
slides ]
Aaron Bohannon, Jeffrey A. Vaughan, and Benjamin C. Pierce.
Relational Lenses: A Language for Updateable Views.
In Principles of Database Systems (PODS), 2006.
Extended version available as University of Pennsylvania technical
report MS-CIS-05-27.
[ bib |
tech report |
.pdf ]
Aaron Bohannon, Jeffrey A. Vaughan, and Benjamin C. Pierce.
Relational Lenses: A language for defining updateable views,
October 2005.
Poster presented at Greater Philadelphia DB/IR Day.
[ bib |
.pdf ]
Michael Y. Levin and Benjamin C. Pierce.
Type-based Optimization for Regular Patterns.
In Database Programming Languages (DBPL), August 2005.
[ bib |
tech report ]
Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and Alan Schmitt.
XML Goes Native: Run-time Representations for Xtatic.
In 14th International Conference on Compiler Construction,
April 2005.
[ bib |
tech report |
conference version ]
Benjamin C. Pierce.
Harmony: The Art of Reconciliation, April 2005.
Invited talk at Trusted Global Computing conference, April
2005.
[ bib |
slides ]
Benjamin C. Pierce.
Fancy Types for XML: Friend or Foe?, April 2005.
Talk at LINKS workshop, April 2005.
[ bib |
slides ]
J. Nathan Foster, Michael B. Greenwald, Christian Kirkegaard, Benjamin C.
Pierce, and Alan Schmitt.
Schema-Directed Data Synchronization.
Technical Report MS-CIS-05-02, University of Pennsylvania, March
2005.
Supersedes MS-CIS-03-42.
[ bib |
tech report ]
Peng Li and Steve Zdancewic.
Downgrading Policies and Relaxed Noninterference.
In Proc. 32nd ACM Symp. on Principles of Programming Languages
(POPL), pages 158–170, January 2005.
[ bib |
.pdf ]
Peng Li and Steve Zdancewic.
Practical Information-flow Control in Web-based Information
Systems.
In Proc. of 18th IEEE Computer Security Foundations Workshop
(CSFW), pages 2–15, 2005.
[ bib |
.pdf ]
Stephen Tse and Steve Zdancewic.
Designing a Security-typed Language with Certificate-based
Declassification.
In Proc. of the 14th European Symposium on Programming (ESOP),
volume 3444, pages 279–294, 2005.
[ bib |
.pdf ]
Peng Li and Steve Zdancewic.
Unifying Confidentiality and Integrity in Downgrading
Policies.
In Proc. of Foundations of Computer Security Workshop (FCS),
2005.
[ bib |
.pdf ]
Michael Hicks, Stephen Tse, Boniface Hicks, and Steve Zdancewic.
Dynamic updating of information-flow policies.
In Proc. of Foundations of Computer Security Workshop (FCS),
2005.
[ bib |
.pdf ]
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster,
Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn,
Stephanie Weirich, and Steve Zdancewic.
Mechanized Metatheory for the Masses: The POPLMark Challenge.
In International Conference on Theorem Proving in Higher Order
Logics (TPHOLs), pages 50–65, 2005.
[ bib |
.pdf ]
Benjamin C. Pierce, editor.
International Conference on Functional Programming (ICFP). ACM
Press, 2005.
[ bib ]
Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and Alan Schmitt.
The Xtatic Experience.
In Workshop on Programming Language Technologies for XML
(PLAN-X), January 2005.
University of Pennsylvania Technical Report MS-CIS-04-24, Oct 2004.
[ bib |
tech report |
slides ]
Eijiro Sumii and Benjamin C. Pierce.
A Bisimulation for Type Abstraction and Recursion.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Long Beach, California, 2005.
Full version in J. ACM, 54 (5), 2007.
[ bib |
short version |
full version ]
Benjamin C. Pierce, editor.
Advanced Topics in Types and Programming Languages.
MIT Press, 2005.
[ bib |
home page ]
Michael Y. Levin.
Run, Xtatic, Run: Efficient Implementation of an Object-Oriented
Language with Regular Pattern Matching.
PhD thesis, University of Pennsylvania, 2005.
[ bib |
.pdf ]
Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and Alan Schmitt.
The Xtatic Compiler and Runtime System, 2005.
[ bib |
source code ]
Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce.
Regular Expression Types for XML.
ACM Transactions on Programming Languages and Systems (TOPLAS),
27(1):46–90, January 2005.
Preliminary version in ICFP 2000.
[ bib |
conference version |
full version ]
Stephanie Weirich.
Type-Safe Cast.
Journal of Functional Programming, 14(6):681–695, November
2004.
[ bib |
http ]
Liang Huang and Stephanie Weirich.
A Design for Type-Directed Programming in Java (Extended
Version).
Technical Report MS-CIS-04-11, University of Pennsylvania, Computer
and Information Science, October 2004.
[ bib |
.ps |
.pdf ]
Vladimir Gapeyev and Benjamin C. Pierce.
Paths into Patterns.
Technical Report MS-CIS-04-25, University of Pennsylvania, October
2004.
[ bib |
tech report ]
Benjamin C. Pierce.
Combinators for Bi-Directional Tree Transformations: A
Linguistic Approach to the View Update Problem, October 2004.
Invited talk at New England Programming Languages Symposium.
[ bib |
slides ]
Stephanie Weirich and Liang Huang.
A Design for Type-Directed Java.
In Viviana Bono, editor, Workshop on Object-Oriented
Developments (WOOD), ENTCS, pages 117–136, August 2004.
[ bib |
.ps |
http ]
Peng Li and Steve Zdancewic.
Advanced Control Flow in Java Card Programming.
In Proceedings of the 2004 ACM SIGPLAN/SIGBED Conference on
Languages, Compilers, and Tools for Embedded Systems (LCTES), pages
165–174, June 2004.
[ bib |
.pdf ]
Stephen Tse and Steve Zdancewic.
Run-time Principals in Information-flow Type Systems.
In IEEE 2004 Symposium on Security and Privacy (Oakland), pages
179–193. IEEE Computer Society Press, May 2004.
[ bib |
.ps |
.pdf ]
Stephen Tse and Steve Zdancewic.
Translating Dependency into Parametricity.
Technical Report MIS-CIS-04-01, University of Pennsylvania, 2004.
[ bib |
.pdf ]
Stephen Tse and Steve Zdancewic.
Translating Dependency into Parametricity.
In Proc. of the 9th ACM SIGPLAN International Conference on
Functional Programming (ICFP), 2004.
[ bib |
.ps |
.pdf ]
Stephen Tse and Steve Zdancewic.
Designing a Security-typed Language with Certificate-based
Declassification.
Technical Report MIS-CIS-04-16, University of Pennsylvania, 2004.
[ bib |
.pdf ]
Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic.
Enforcing Robust Declassification.
In Proc. of 17th IEEE Computer Security Foundations Workshop
(CSFW), pages 172–186, 2004.
[ bib |
.pdf ]
Steve Zdancewic.
Challenges for Information-flow Security.
In Proceedings of the 1st International Workshop on the
Programming Language Interference and Dependence (PLID’04), 2004.
(5 pages).
[ bib |
.pdf ]
Eijiro Sumii and Benjamin C. Pierce.
A Bisimulation for Dynamic Sealing.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Venice, Italy, 2004.
Full version in Theoretical Computer Science 375 (2007),
169–192.
[ bib |
conference version ]
Benjamin C. Pierce and Jérôme Vouillon.
What’s in Unison? A Formal Specification and Reference
Implementation of a File Synchronizer.
Technical Report MS-CIS-03-36, Dept. of Computer and Information
Science, University of Pennsylvania, 2004.
[ bib |
tech report ]
Peng Li, Yun Mao, and Steve Zdancewic.
Information Integrity Policies.
In Proceedings of the Workshop on Formal Aspects in Security &
Trust (FAST), September 2003.
[ bib |
.ps |
.pdf ]
Benjamin C. Pierce.
Harmony: A Synchronization Framework for Tree-Structured Data,
September 2003.
Slides from a talk presented in several places (Cambridge, Edinburgh,
Philadelphia, Princeton) in Fall 2003.
[ bib |
slides ]
David Walker, Steve Zdancewic, and Jay Ligatti.
A Theory of Aspects.
In Proc. of the 8th ACM SIGPLAN International Conference on
Functional Programming (ICFP), pages 127–139, Upsala, Sweden, August 2003.
[ bib |
.ps |
.pdf ]
Steve Zdancewic and Andrew C. Myers.
Observational Determinism for Concurrent Program Security.
In Proc. of 16th IEEE Computer Security Foundations Workshop
(CSFW), pages 29–45, Asilomar, CA, July 2003.
[ bib |
.ps |
.pdf ]
Usa Sammapun, Raman Sharykin, Margaret Delap, Myong Kim, and Steve Zdancewic.
Formalizing Java-MaC.
In Proceedings of the Third Runtime Verification Workshop,
pages 171–190. Electronic Notes in Theoretical Computer Science, July 2003.
[ bib |
.ps |
.pdf ]
Haruo Hosoya and Benjamin C. Pierce.
XDuce: A Statically Typed XML Processing Language.
ACM Transactions on Internet Technology, 3(2):117–148, May
2003.
[ bib |
official version ]
Michael Greenwald, Carl A. Gunter, Björn Knutsson, Andre Scedrov,
Jonathan M. Smith, and Steve Zdancewic.
Computer Security is Not a Science (but it should be).
In Proceedings of the Large-Scale Network Security Workshop,
March 2003.
[ bib |
.ps |
.pdf ]
Steve Zdancewic.
A Type System for Robust Declassification.
In Proceedings of the Nineteenth Conference on the Mathematical
Foundations of Programming Semantics (MFPS). Electronic Notes in Theoretical
Computer Science, March 2003.
(16 pages).
[ bib |
.ps |
.pdf ]
Michael Y. Levin and Benjamin C. Pierce.
TinkerType: A Language for Playing with Formal Systems.
Journal of Functional Programming, 13(2), March 2003.
A preliminary version appeared as an invited paper at the
Logical Frameworks and Metalanguages Workshop (LFM), June 2000.
[ bib |
source code |
full version |
slides ]
Stephen Tse and Steve Zdancewic.
Run-time Principals in Information-flow Type Systems.
Technical Report MS-CIS-03-39, University of Pennsylvania, 2003.
The conference version appears in IEEE Security and Privacy 2004.
[ bib |
.ps |
.pdf ]
Lantian Zheng, Stephen Chong, Steve Zdancewic, and Andrew C. Myers.
Building Secure Distributed Systems Using Replication and
Partitioning.
In IEEE 2003 Symposium on Security and Privacy (Oakland),
pages 236–250. IEEE Computer Society Press, 2003.
[ bib |
.ps |
.pdf ]
Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt.
A Language for Bi-Directional Tree Transformations.
Manuscript; available at
http://www.cis.upenn.edu/ bcpierce/papers/lenses.pdf, 2003.
[ bib ]
Benjamin C. Pierce, Alan Schmitt, and Michael B. Greenwald.
Bringing Harmony to Optimism: A Synchronization Framework
for Heterogeneous Tree-Structured Data.
Technical Report MS-CIS-03-42, University of Pennsylvania, 2003.
Superseded by MS-CIS-05-02.
[ bib |
tech report ]
Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt.
A Language for Bi-Directional Tree Transformations.
Technical Report MS-CIS-03-08, University of Pennsylvania, 2003.
Revised April 2004.
[ bib ]
M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, editors.
Software Security – Theories and Systems, number 2609 in
Lecture Notes in Computer Science. Springer-Verlag, 2003.
Revised papers from the Mext-NSF-JSPS International Symposium on
Software Security, Tokyo, Japan, November 8-10, 2002.
[ bib ]
Vladimir Gapeyev and Benjamin C. Pierce.
Regular Object Types.
In European Conference on Object-Oriented Programming (ECOOP),
Darmstadt, Germany, 2003.
A preliminary version was presented at FOOL ’03.
[ bib |
short version |
slides ]
Eijiro Sumii and Benjamin C. Pierce.
Logical Relations for Encryption.
Journal of Computer Security, 11(4):521–554, 2003.
Extended abstract appeared in ph14th IEEE Computer Security
Foundations Workshop, pp. 256–269, 2001.
[ bib |
conference version ]
Trevor Jim, Benjamin C. Pierce, and Jérôme Vouillon.
How to Build a File Synchronizer.
Manuscript, 2003.
[ bib ]
Vladimir Gapeyev, Michael Levin, and Benjamin Pierce.
Recursive Subtyping Revealed.
Journal of Functional Programming, 12(6):511–548, 2003.
Preliminary version in International Conference on Functional
Programming (ICFP), 2000. Also appears as Chapter 21 of Types and
Programming Languages by Benjamin C. Pierce (MIT Press, 2002).
[ bib |
conference version ]
Benjamin C. Pierce.
Types and Programming Languages: The Next Generation, 2003.
Invited tutorial at Logic in Computer Science (LICS).
[ bib |
slides ]
Stephanie Weirich.
Programming With Types.
PhD thesis, Cornell University, August 2002.
[ bib |
.ps |
.pdf ]
Atsushi Igarashi and Benjamin C. Pierce.
On Inner Classes.
Information and Computation, 177(1):56–89, August 2002.
A special issue with papers from the 7th International Workshop on
Foundations of Object-Oriented Languages (FOOL), informal proceedings.
An earlier version appeared in \bgroup Proceedings of the 14th European
Conference on Object-Oriented Programming (ECOOP), Springer LNCS 1850,
pages 129–153.
[ bib |
tech report |
conference version ]
Benjamin C. Pierce.
Synchronize globally, compute locally, July 2002.
Keynote address at Research Day on Global Computing, EFPL,
Lausanne.
[ bib |
slides ]
Stephanie Weirich.
Higher-Order Intensional Type Analysis.
In Daniel Le Métayer, editor, 11th European Symposium on
Programming (ESOP), pages 98–114, Grenoble, France, April 2002.
[ bib |
.ps |
.pdf ]
Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers.
Secure Program Partitioning.
Transactions on Computer Systems, 20(3):283–328, 2002.
[ bib |
.ps |
.pdf ]
Steve Zdancewic and Andrew C. Myers.
Secure Information Flow via Linear Continuations.
Higher Order and Symbolic Computation, 15(2/3):209–234, 2002.
[ bib |
.ps |
.pdf ]
Benjamin C. Pierce.
Types and Programming Languages.
MIT Press, 2002.
[ bib |
errata |
home page ]
Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers.
Untrusted Hosts and Confidentiality: Secure Program
Partitioning.
In Proc. 18th ACM Symp. on Operating System Principles
(SOSP), volume 35(5) of Operating Systems Review, pages 1–14, Banff,
Canada, October 2001.
[ bib |
.ps |
.pdf ]
Steve Zdancewic and Andrew C. Myers.
Robust Declassification.
In Proc. of 14th IEEE Computer Security Foundations Workshop
(CSFW), pages 15–23, Cape Breton, Canada, June 2001.
[ bib |
.ps |
.pdf ]
Steve Zdancewic and Andrew C. Myers.
Secure Information Flow and CPS.
In Proc. of the 10th European Symposium on Programming (ESOP),
volume 2028 of Lecture Notes in Computer Science, pages 46–61, April
2001.
[ bib |
.ps |
.pdf ]
Stephanie Weirich.
Encoding Intensional Type Analysis.
In D. Sands, editor, 10th European Symposium on Programming
(ESOP), pages 92–106, Genova, Italy, April 2001.
[ bib |
http |
.ps |
.pdf ]
Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers.
Secure Program Partitioning.
Technical Report 2001-1846, Computer Science Dept., Cornell
University, 2001.
[ bib |
.ps |
.pdf ]
Michael Hicks, Stephanie Weirich, and Karl Crary.
Safe and Flexible Dynamic Linking of Native Code.
In R. Harper, editor, Types in Compilation: Third International
Workshop, TIC 2000; Montreal, Canada, September 21, 2000; Revised Selected
Papers, volume 2071 of Lecture Notes in Computer Science, pages
147–176. Springer, 2001.
[ bib |
http |
.ps.gz |
.pdf ]
Naoki Kobayashi and Benjamin C. Pierce, editors.
Theoretical Aspects of Computer Software (TACS), 4th
International Symposium, number 2215 in Lecture Notes in Computer Science.
Springer-Verlag, 2001.
[ bib ]
Benjamin C. Pierce and Jérôme Vouillon.
Unison: A File Synchronizer and its Specification.
Manuscript, 2001.
[ bib ]
Eijiro Sumii and Benjamin Pierce.
The Cryptographic λ-Calculus: Syntax, Semantics, Type
System and Logical Relation (in Japanese).
In Informal Proceedings of JSSST Workshop on Programming and
Programming Languages (PPL2001), 2001.
Best paper prize.
[ bib ]
Haruo Hosoya and Benjamin C. Pierce.
Regular Expression Pattern Matching.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), London, England, 2001.
Full version in Journal of Functional Programming, 13(6), Nov.
2003, pp. 961–1004.
[ bib |
full version ]
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler.
A Recipe for Raw Types.
In Workshop on Foundations of Object-Oriented Languages (FOOL),
2001.
[ bib |
short version ]
Benjamin C. Pierce.
Unison: A file synchronizer and its specification, 2001.
Invited talk at Theoretical Aspects of Computer Software
(TACS), Sendai, Japan.
[ bib |
slides ]
Benjamin C. Pierce.
File Synchronization: Theory and Practice, 2001.
[ bib |
slides ]
Benjamin C. Pierce.
Global Computing: Some Questions for FOOLs, 2001.
Invited talk at FOOL workshop.
[ bib |
slides ]
Benjamin C. Pierce and David N. Turner.
The Pict Programming Language, 2001.
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!).
[ bib |
home page ]
Dan Grossman, Greg Morrisett, and Steve Zdancewic.
Syntactic Type Abstraction.
Transactions on Programming Languages and Systems,
22(6):1037–1080, November 2000.
[ bib |
.ps |
.pdf ]
Stephanie Weirich.
Type-Safe Cast: Functional Pearl.
In Proceedings of the fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 58–67, Montreal, Canada,
September 2000.
[ bib |
.ps |
.pdf ]
Benjamin C. Pierce.
Module Systems: A Guide for the Perplexed, September 2000.
Invited talk at ICFP, Montreal.
[ bib ]
Benjamin Pierce and Eijiro Sumii.
Relating Cryptography and Polymorphism, July 2000.
Some parts superseded by [381] (Sumii and Pierce,
2001).
[ bib |
manuscript ]
Michael Y. Levin and Benjamin C. Pierce.
TinkerType: A Language for Playing with Formal Systems.
Technical report, June 2000.
Invited talk (submitted for journal publication).
[ bib ]
Haruo Hosoya and Benjamin C. Pierce.
XDuce: A Typed XML Processing Language (Preliminary
Report).
In Dan Suciu and Gottfried Vossen, editors, International
Workshop on the Web and Databases (WebDB), May 2000.
Reprinted in The Web and Databases, Selected Papers, Springer
LNCS volume 1997, 2001.
[ bib |
conference version ]
Michael Hicks and Stephanie Weirich.
A Calculus for Dynamic Loading.
Technical Report MS-CIS-00-07, University of Pennsylvania, April
2000.
[ bib |
www: ]
Arnaud Sahuguet, Benjamin Pierce, and Val Tannen.
Distributed Query Optimization: Can Mobile Agents Help?,
February 2000.
[ bib ]
Arnaud Sahuguet, Benjamin Pierce, and Val Tannen.
Chaining, Referral, Subscription, Leasing: New Mechanisms in
Distributed Query Optimization, February 2000.
[ bib ]
Steve Zdancewic and Andrew C. Myers.
Confidentiality and Integrity with Untrusted Hosts.
Technical Report 2000-1810, Computer Science Dept., Cornell
University, 2000.
[ bib |
.ps |
.pdf ]
Karl Crary and Stephanie Weirich.
Resource Bound Certification.
In The Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL), pages 184–198, Boston, MA, USA,
January 2000.
[ bib |
.ps.gz |
.pdf ]
Vladimir Gapeyev, Michael Levin, and Benjamin Pierce.
Recursive Subtyping Revealed.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), Montreal, Canada, 2000.
To appear in Journal of Functional Programming.
[ bib ]
Benjamin C. Pierce and David N. Turner.
Pict: A Programming Language Based on the Pi-Calculus.
In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors,
Proof, Language and Interaction: Essays in Honour of Robin Milner, pages
455–494. MIT Press, 2000.
[ bib |
full version ]
Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce.
Location Independence for Mobile Agents.
2000.
To appear in an edited collection of papers (in Springer LNCS) from
the Workshop on Internet Programming Languages, June 1998, Loyola
University.
[ bib ]
Benjamin C. Pierce.
Advanced Module Systems: A Guide for the Perplexed, 2000.
Invited tutorial at International Conference on Functional
Programming (ICFP).
[ bib |
slides ]
Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce.
Comparing Object Encodings.
Information and Computation, 155(1/2):108–133, November 1999.
Special issue of papers from 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.
[ bib |
.ps ]
Atsushi Igarashi, Benjamin Pierce, and Philip Wadler.
Featherweight Java: A Minimal Core Calculus for Java and
GJ.
In ACM SIGPLAN Conference on Object Oriented
Programming: Systems, Languages, and Applications (OOPSLA),
October 1999.
Full version in ACM Transactions on Programming Languages and Systems
(TOPLAS), 23(3), May 2001.
[ bib |
conference version |
full version ]
Steve Zdancewic, Dan Grossman, and Greg Morrisett.
Principals in Programming Languages: A Syntactic Proof
Technique.
In Proc. of the 4th ACM SIGPLAN International Conference on
Functional Programming (ICFP), pages 197–207, Paris, France, September
1999.
[ bib |
.ps |
.pdf ]
Karl Crary and Stephanie Weirich.
Flexible Type Analysis.
In Proceedings of the fourth ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 233–248, Paris, France,
September 1999.
[ bib |
.ps.gz |
.pdf ]
Peter Sewell, Pawel Wojciechowski, and Benjamin Pierce.
Location Independence for Mobile Agents.
In H. E. Bal, B. Belkhouche, and L. Cardelli, editors,
Proceedings of ICCL ’98, volume 1686 of lncs. Springer-Verlag,
September 1999.
An earlier version with title Location-Independent Communication
for Mobile Agents: a Two-Level Architecture appeared as Technical Report
462, Computer Laboratory, University of Cambridge, April 1999.
[ bib |
tech report |
official version ]
Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner.
Linearity and the Pi-Calculus.
ACM Transactions on Programming Languages and Systems,
21(5):914–947, September 1999.
Summary in POPL 1996.
[ bib |
full version ]
Steve Zdancewic and Dan Grossman.
Principals in Programming Languages: Technical Results.
Technical Report TR99-1752, Computer Science Dept., Cornell
University, June 1999.
[ bib |
.ps |
.pdf ]
Haruo Hosoya and Benjamin C. Pierce.
How Good is Local Type Inference?
Technical Report MS-CIS-99-17, University of Pennsylvania, June 1999.
[ bib |
tech report ]
Atsushi Igarashi and Benjamin C. Pierce.
Foundations for Virtual Types.
In European Conference on Object-Oriented Programming (ECOOP),
Lisbon, Portugal, June 1999.
Also in informal proceedings of the Workshop on Foundations of
Object-Oriented Languages (FOOL), January 1999. Full version in
Information and Computation, 175(1): 34–49, May 2002.
[ bib |
.ps ]
Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick
Smith, David Walker, Stephanie Weirich, and Steve Zdancewic.
TALx86: A Realistic Typed Assembly Language.
In Second ACM SIGPLAN Workshop on Compiler Support for
System Software, pages 25–35, Atlanta, GA, USA, May 1999.
Published as INRIA research report number 0228, March 1999.
[ bib |
.ps |
.pdf ]
Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick
Smith, David Walker, Stephanie Weirich, and Steve Zdancewic.
TALx86: A Realistic Typed Assembly Language.
In 2nd ACM SIGPLAN Workshop on Compiler Support for System
Software, pages 25–35, 1999.
[ bib |
.ps |
.pdf ]
Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce.
Location-Independent Communication for Mobile Agents: a
Two-Level Architecture.
Technical Report 462, Computer Laboratory, University of Cambridge,
1999.
[ bib ]
S. Balasubramaniam and Benjamin C. Pierce.
What is a file synchronizer?
In Fourth Annual ACM/IEEE International Conference on Mobile
Computing and Networking (MobiCom ’98), October 1998.
Full version available as Indiana University CSCI technical report
#507, April 1998.
[ bib |
tech report |
conference version |
slides ]
Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type Erasure Semantics.
In Proceedings of the third ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 301–313, Baltimore, MD,
USA, September 1998.
[ bib |
.ps |
.pdf ]
Peter Buneman and Benjamin Pierce.
Union Types for Semistructured Data.
In Internet Programming Languages. Springer-Verlag, September
1998.
Proceedings of the International Database Programming Languages
Workshop. LNCS 1686.
[ bib |
conference version ]
Benjamin C. Pierce.
Type Systems for Concurrent Calculi, September 1998.
Invited tutorial at CONCUR, Nice, France.
[ bib ]
S. Balasubramaniam and Benjamin C. Pierce.
File Synchronization.
Technical Report 507, Computer Science Department, Indiana
University, April 1998.
[ bib ]
Haruo Hosoya, Benjamin C. Pierce, and David N. Turner.
Datatypes and Subtyping.
Manuscript, 1998.
[ bib |
.ps ]
Benjamin C. Pierce, Trevor Jim Sundar Balasubramaniam, Insup Lee, and Insik
Shin.
Snc: a file synchronizer, 1998.
(Superseded by Unison.).
[ bib ]
Benjamin C. Pierce.
Type Systems for Concurrent Calculi, 1998.
Invited tutorial at CONCUR.
[ bib |
slides ]
Martin Hofmann and Benjamin C. Pierce.
Type Destructors.
In Didier Rémy, editor, Informal proceedings of the Fourth
International Workshop on Foundations of Object-Oriented Languages (FOOL),
January 1998.
Full version in Information and Computation, 172(1)29–62
(2002).
[ bib |
conference version ]
Benjamin C. Pierce and David N. Turner.
Local Type Inference.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), San Diego, California, 1998.
Full version in ACM Transactions on Programming Languages
and Systems (TOPLAS), 22(1), January 2000, pp. 1–44.
[ bib |
tech report |
conference version |
full version ]
Giorgio Ghelli and Benjamin Pierce.
Bounded Existentials and Minimal Typing.
Theoretical Computer Science, 193:75–96, 1998.
Circulated in manuscript form in 1992.
[ bib ]
Benjamin C. Pierce.
Languages for Programming the Web, December 1997.
Course materials for a graduate seminar on the theory and practice of
mobile agent programming. Available through http://www.cis.upenn.edu/simbcpierce/courses/629.
[ bib ]
Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce.
Comparing Object Encodings.
In International Symposium on Theoretical Aspects of Computer
Software (TACS), September 1997.
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 Information and Computation,
155(1–2):108-133, 1999.
[ bib ]
Benjamin C. Pierce.
Intersection Types and Bounded Polymorphism.
Mathematical Structures in Computer Science, 7(2):129–193,
April 1997.
Summary in Typed Lambda Calculi and Applications, March 1993,
pp. 346–360.
[ bib ]
Benjamin C. Pierce.
Review of A Theory of Objects, by Abadi and Cardelli.
The Computer Journal, 40(5):297–298, 1997.
[ bib |
.ps ]
Benjamin C. Pierce.
Programming in the Pi-Calculus: A Tutorial Introduction to
Pict.
Available electronically, 1997.
[ bib ]
Benjamin C. Pierce and David N. Turner.
Pict: A Programming Language Based on the Pi-Calculus, 1997.
http://www.cis.upenn.edu/ bcpierce/papers/pict.
[ bib ]
Benjamin C. Pierce and David N. Turner.
Pict Libraries Manual.
Available electronically, 1997.
[ bib ]
Benjamin C. Pierce and David N. Turner.
Pict Language Definition.
Available electronically, 1997.
[ bib ]
Benjamin C. Pierce and David N. Turner.
Local Type Inference.
Technical Report 493, Computer Science Department, Indiana
University, 1997.
[ bib ]
Benjamin C. Pierce and David N. Turner.
Local Type Argument Synthesis with Bounded Quantification.
Technical Report 495, Computer Science Department, Indiana
University, January 1997.
[ bib |
tech report ]
Benjamin Pierce and Martin Steffen.
Higher-Order Subtyping.
Theoretical Computer Science, 176(1–2):235–282, 1997.
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ät Erlangen-Nürnberg Interner
Bericht IMMD7-01/94, January 1994.
[ bib ]
Benjamin C. Pierce.
Bounded Quantification with Bottom.
Technical Report 492, Computer Science Department, Indiana
University, 1997.
[ bib |
tech report ]
Benjamin Pierce and Davide Sangiorgi.
Behavioral Equivalence in the Polymorphic Pi-Calculus.
In Principles of Programming Languages (POPL), pages 531–584,
1997.
Full version in Journal of the Association for Computing
Machinery (JACM), 47(3), May 2000.
[ bib |
full version ]
Adriana B. Compagnoni and Benjamin C. Pierce.
Intersection Types and Multiple Inheritance.
Mathematical Structures in Computer Science, 6(5):469–501,
October 1996.
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”.
[ bib ]
Uwe Nestmann and Benjamin C. Pierce.
Decoding Choice Encodings.
In Proceedings of CONCUR ’96, August 1996.
Full version in Information and Computation,
163(1): 1–59 (2000).
[ bib |
full version ]
Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce.
Comparing Object Encodings.
In Invited lecture at Third Workshop on Foundations of Object
Oriented Languages (FOOL 3), July 1996.
[ bib ]
Benjamin C. Pierce.
Processes, Types, and Observations, March 1996.
Invited lecture at Formal Methods on Open, Object-Based
Distributed Systems (FMOODS), Paris.
[ bib ]
Benjamin C. Pierce.
Even simpler type-theoretic foundations for OOP.
Manuscript (circulated electronically), March 1996.
[ bib ]
Benjamin C. Pierce.
Types.
Lecture notes for an undergraduate course at Cambridge University,
February 1996.
[ bib ]
Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and
Matthias Felleisen.
Catching Bugs in the Web of Program Invariants.
In ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI), pages 23–32, 1996.
[ bib |
.ps |
.pdf ]
Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, the Hopkins Objects Group
(Jonathan Eifrig, Scott Smith, Valery Trifonov), Gary T. Leavens, and
Benjamin Pierce.
On Binary Methods.
Theory and Practice of Object Systems, 1(3):221–242, 1996.
[ bib |
.ps ]
Adriana B. Compagnoni and Benjamin C. Pierce.
Multiple Inheritance via Intersection Types.
Mathematical Structures in Computer Science, 1996.
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.
[ bib ]
Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner.
Linearity and the Pi-Calculus.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), St. Petersburg Beach, Florida, 1996.
Full version in ACM Transactions on Programming Languages
and Systems, 21(5), pp. 914–947, September 1999.
[ bib ]
Benjamin C. Pierce.
Foundational Calculi for Programming Languages.
In Allen B. Tucker, editor, Handbook of Computer Science and
Engineering, chapter 139. CRC Press, 1996.
[ bib |
full version ]
Benjamin C. Pierce.
Using Types to Compare Objects and ADTs, October 1995.
Invited lecture at Horizon Day, Indiana University.
[ bib ]
Martin Hofmann and Benjamin Pierce.
A Unifying Type-Theoretic Framework for Objects.
Journal of Functional Programming, 5(4):593–635, October 1995.
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.
[ bib |
.ps ]
Benjamin C. Pierce.
Linearity and the Pi-Calculus, August 1995.
Invited lecture at Advances in Type Systems for Computation,
Cambridge, England.
[ bib ]
Benjamin C. Pierce and David N. Turner.
Concurrent Objects in a Process Calculus.
In Takayasu Ito and Akinori Yonezawa, editors, Theory and
Practice of Parallel Programming (TPPP), Sendai, Japan (Nov. 1994), number
907 in Lecture Notes in Computer Science, pages 187–215. Springer-Verlag,
April 1995.
[ bib |
short version |
.ps ]
Martin Hofmann and Benjamin Pierce.
Positive Subtyping.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), San Francisco, California, pages
186–197, January 1995.
Full version in Information and Computation, volume
126, number 1, April 1996. Also available as University of Edinburgh
technical report ECS-LFCS-94-303, September 1994.
[ bib |
.ps ]
Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner.
Linearity and the Pi-Calculus, 1995.
Technical report, Department of Information Science, University of
Tokyo and Computer Laboratory, University of Cambridge.
[ bib ]
Martín Abadi, Luca Cardelli, Benjamin Pierce, and Didier Rémy.
Dynamic Typing in Polymorphic Languages.
Journal of Functional Programming, 5(1):111–130, January 1995.
Summary in ACM SIGPLAN Workshop on ML and its
Applications, June 1992.
[ bib ]
Giuseppe Castagna and Benjamin Pierce.
Corrigendum: Decidable Bounded Quantification.
In Proceedings of the Twenty-Second ACM SIGPLAN–SIGACT
Symposium on Principles of Programming Languages (POPL), Portland,
Oregon. ACM, January 1995.
[ bib |
.ps ]
Benjamin C. Pierce.
Concurrent Objects in a Process Calculus, November 1994.
Invited lecture at Theory and Practice of Parallel Programming
(TPPP), Sendai, Japan.
[ bib ]
Martin Hofmann and Benjamin Pierce.
Positive Subtyping.
Technical Report ECS-LFCS-94-303, LFCS, University of Edinburgh,
September 1994.
[ bib ]
Benjamin C. Pierce.
Bounded Quantification is Undecidable.
Information and Computation, 112(1):131–165, July 1994.
Also in C. A. Gunter and J. C. Mitchell, editors, Theoretical
Aspects of Object-Oriented Programming: Types, Semantics, and Language
Design, MIT Press, 1994. Summary in ACM SIGPLAN–SIGACT
Symposium on Principles of Programming Languages (POPL),
Albuquerque, New Mexico.
[ bib |
conference version ]
Benjamin C. Pierce and David N. Turner.
Simple Type-Theoretic Foundations for Object-Oriented
Programming.
Journal of Functional Programming, 4(2):207–247, April 1994.
Summary in ACM SIGPLAN–SIGACT Symposium on
Principles of Programming Languages (POPL), Charleston, South
Carolina, 1993.
[ bib |
conference version |
.ps |
.pdf ]
Benjamin C. Pierce.
Woggles from Oz: Writing Interactive Fiction.
Leonardo: Journal of the International Society for the Arts,
Sciences, and Technology, 1994.
Expanded version available electronically.
[ bib ]
Martin Steffen and Benjamin Pierce.
Higher-Order Subtyping.
Technical Report ECS-LFCS-94-280, LFCS, University of Edinburgh,
January 1994.
Also available as Universität Erlangen-Nürnberg Interner Bericht
IMMD7-01/94. To appear in Theoretical Computer Science.
[ bib ]
Benjamin C. Pierce and Martin Steffen.
Higher-Order Subtyping.
In IFIP Working Conference on Programming Concepts, Methods and
Calculi (PROCOMET), 1994.
Full version in Theoretical Computer Science,
vol. 176, no. 1–2, pp. 235–282, 1997 (corrigendum in TCS vol. 184 (1997),
p. 247).
[ bib |
tech report ]
Giuseppe Castagna and Benjamin Pierce.
Decidable Bounded Quantification.
In Proceedings of the Twenty-First ACM SIGPLAN–SIGACT
Symposium on Principles of Programming Languages (POPL), Portland,
Oregon. ACM, January 1994.
[ bib |
.ps ]
Benjamin C. Pierce, Didier Rémy, and David N. Turner.
A Typed Higher-Order Programming Language Based on the
Pi-Calculus.
In Workshop on Type Theory and its Application to Computer
Systems, Kyoto University, July 1993.
[ bib ]
Benjamin C. Pierce.
A Typed Higher-Order Programming Language Based on the
Pi-Calculus, July 1993.
Invited lecture at Workshop on Type Theory and its Application
to Computer Systems, Kyoto University.
[ bib ]
Benjamin C. Pierce.
Mutable Objects.
Draft report; available electronically, June 1993.
[ bib |
.ps ]
Benjamin C. Pierce and David N. Turner.
Statically Typed Friendly Functions via Partially Abstract
Types.
Technical Report ECS-LFCS-93-256, University of Edinburgh, LFCS,
April 1993.
Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899.
[ bib |
.ps ]
Benjamin Pierce.
Object-Oriented Programming in Typed Lambda-Calculus: Exercises
and Solutions.
Lecture notes for 1992 Frankische OOrientierungstage, University of
Erlangen, Germany (revised version), April 1993.
[ bib ]
Benjamin C. Pierce.
A Model of Delegation Based on Existential Types.
Available electronically, April 1993.
[ bib |
.ps ]
Benjamin C. Pierce.
Typage des Traits Orientés-Objets, February 1993.
Invited lecture at Journeés Francophones des Langages
Applicatifs, Annecy, France.
[ bib ]
Benjamin C. Pierce.
F-Omega-Sub User’s Manual, Version 1.4.
Available by FTP as part of the fomega implementation, February
1993.
[ bib ]
Benjamin C. Pierce.
F-Omega-Sub: a polymorphic λ-calculus with
higher-order subtyping and object-oriented extensions, 1993.
[ bib ]
Benjamin C. Pierce and Davide Sangiorgi.
Typing and Subtyping for Mobile Processes.
In Logic in Computer Science, 1993.
Full version in Mathematical Structures in Computer
Science , Vol. 6, No. 5, 1996.
[ bib |
full version ]
Benjamin C. Pierce and David N. Turner.
Object-Oriented Programming Without Recursive Types.
In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Charleston, South Carolina, pages
299–312, January 1993.
[ bib ]
Benjamin C. Pierce and Robert Pollack.
Higher-Order Subtyping.
Unpublished manuscript, August 1992.
[ bib ]
Giorgio Ghelli and Benjamin Pierce.
Bounded Existentials and Minimal Typing, 1992.
Circulated in manuscript form. Full version in Theoretical
Computer Science, 193(1–2):75–96, February 1998.
[ bib |
.ps ]
Martin Hofmann and Benjamin Pierce.
An Abstract View of Objects and Subtyping (Preliminary Report).
Technical Report ECS-LFCS-92-226, University of Edinburgh, LFCS,
1992.
[ bib ]
Benjamin C. Pierce.
Programming with Intersection Types and Bounded Polymorphism.
PhD thesis, Carnegie Mellon University, December 1991.
Available as School of Computer Science technical report
CMU-CS-91-205.
[ bib ]
Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin.
Dynamic Typing in a Statically Typed Language.
ACM Transactions on Programming Languages and Systems,
13(2):237–268, April 1991.
Summary in ACM Symposium on Principles of
Programming Languages (POPL), Austin, Texas, 1989.
[ bib ]
Martín Abadi, Benjamin Pierce, and Gordon Plotkin.
Faithful Ideal Models for Recursive Polymorphic Types.
International Journal of Foundations of Computer Science,
2(1):1–21, March 1991.
Summary in Fourth Annual Symposium on Logic in Computer Science,
June, 1989.
[ bib ]
Benjamin C. Pierce.
Programming with Intersection Types, Union Types, and
Polymorphism.
Technical Report CMU-CS-91-106, Carnegie Mellon University, February
1991.
[ bib ]
Benjamin C. Pierce.
Fmeet: a polymorphic λ-calculus with intersection
types, 1991.
[ bib ]
Benjamin C. Pierce.
Basic Category Theory for Computer Scientists.
MIT Press, 1991.
[ bib ]
Robert Harper and Benjamin Pierce.
A Record Calculus Based on Symmetric Concatenation.
In ACM Symposium on Principles of Programming
Languages (POPL), Orlando, Florida, pages 131–142, January 1991.
Extended version available as Carnegie Mellon Technical Report
CMU-CS-90-157.
[ bib ]
Benjamin C. Pierce.
Preliminary Investigation of a Calculus with Intersection and
Union Types.
Unpublished manuscript, June 1990.
[ bib ]
Robert W. Harper and Benjamin C. Pierce.
Extensible Records Without Subsumption.
Technical Report CMU-CS-90-102, School of Computer Science, Carnegie
Mellon University, February 1990.
[ bib ]
Benjamin Pierce.
Bounded Quantification and Intersection Types.
Thesis proposal (unpublished), September 1989.
[ bib ]
Benjamin Pierce.
A Decision Procedure for the Subtype Relation on Intersection
Types with Bounded Variables.
Technical Report CMU-CS-89-169, School of Computer Science, Carnegie
Mellon University, September 1989.
[ bib ]
Benjamin Pierce, Scott Dietzen, and Spiro Michaylov.
Programming in Higher-order Typed Lambda-Calculi.
Technical Report CMU-CS-89-111, Carnegie Mellon University, March
1989.
[ bib |
errata |
tech report ]
A. N. Habermann, Charles Krueger, Benjamin Pierce, Barbara Staudt, and John
Wenn.
Programming with Views.
Technical Report CMU-CS-87-177, Carnegie Mellon University, Computer
Science Department, January 1988.
[ bib ]
Benjamin C. Pierce.
Artemis: a graphics editor for circuit diagrams, 1986.
Used internally at DEC Western Research Lab for the design of the
Titan processor and power/packaging.
[ bib ]
T. Larrabee, K. McCall, C. Mitchell, and B. C. Pierce.
Gambit: A Video Game Programming Language.
Project report for Stanford CS-242 (Programming Language Design),
December 1982.
See also: Larrabee, T. and Mitchell, C. “Gambit: A Prototyping
Approach to Video Game Design.” IEEE Software, Vol. 1 No. 4, Oct. 1984.
[ bib ]
B. C. Pierce.
Gridapple: A Microcomputer-Based Geographic Information
System.
In Harvard Computer Graphics Week, July 1982.
Reprinted in Marble, D., et al, Basic Readings in Geographic
Information Systems. Williamsville, NY: SPAD Systems, Ltd., 1984.
[ bib ]
B. C. Pierce.
A Microcomputer-Based Geographic Information System.
In Proceedings of the Seventh West Coast Computer Faire, March
1982.
[ bib ]
Benjamin C. Pierce.
Arc-Info plotting and display subsystem, 1982.
Marketed by Environmental Systems Research Institute, Redlands, CA,
USA.
[ bib ]
Benjamin C. Pierce.
Gridapple: an implementation of the ESRI Grid
system for the Apple-II, 1981.
Marketed by Environmental Systems Research Institute, Redlands, CA.
[ bib ]