PLClub Publications

Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, 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. To appear. [ bib | http ]

Benjamin C. Pierce. The Curse of Knowledge, January 2017. Talk at Programming Languages Mentoring Workshop (PLMW). [ bib | slides ]

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, 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 ]

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 ]

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 ]

Benjamin C. Pierce. The Science of Deep Specification, November 2016. Invited keynote at SPLASH / OOPSLA. [ bib | slides ]

Yannis Juglaret, Catalin Hritcu, 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 ]

Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Beginner's Luck: A Language for Random Generators. Draft, arXiv:1607.05443, July 2016. [ bib | http ]

Benjamin C. Pierce. The Science of Deep Specification, May 2016. High-Confidence Software Systems (HCSS). [ bib | slides ]

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 ]

Steven Keuchel, Stephanie Weirich, and Thomas Tom Schrijvers. InfraGen: Binder Boilerplate at Scale. In European Symposium on Programming (ESOP), pages 419-445, April 2016. [ bib ]

Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. Visible Type Application. In European Symposium on Programming (ESOP), pages 229-254, April 2016. [ bib | .pdf ]

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2016. Version 4.0. http://www.cis.upenn.edu/ bcpierce/sf. [ bib ]

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 ]

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 ]

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 ]

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, 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, 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, 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, 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 ]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe zero-cost coercions for Haskell. Journal of Functional Programming, 26, 007 2016. [ bib | DOI | http | .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 | .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 ]

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 ]

Sulekha Kulkarni, Ravi Mangal, Xin Zhang, and Mayur Naik. Accelerating Program Analyses by Cross-Program Training. In Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. [ bib | slides | .pdf ]

Xujie Si, Xin Zhang, Vasco Manquinho, Mikolas Janota, Alexey Ignatiev, and Mayur Naik. On Incremental Core-Guided MaxSAT Solving. In International Conference on Principles and Practice of Constraint Programming (CP), 2016. [ bib | slides | .pdf ]

Insu Yun, Changwoo Min, Xujie Si, Yeongjin Jang, Taesoo Kim, and Mayur Naik. APISan: Sanitizing API Usages through Semantic Cross-checking. In USENIX Security Symposium, 2016. [ bib | slides | .pdf ]

Ravi Mangal, Xin Zhang, Aditya Kamath, Aditya Nori, and Mayur Naik. Scaling Relational Inference Using Proofs and Refutations. In Conference on Artificial Intelligence (AAAI), 2016. [ bib | .pdf ]

Xin Zhang, Ravi Mangal, Aditya Nori, and Mayur Naik. Query-Guided Maximum Satisfiability. In Symposium on Principles of Programming Languages (POPL), 2016. [ bib | slides | .pdf ]

R. Alur, S. Moarref, and U. Topcu. Compositional Synthesis of Reactive Controllers for Multi-agent Systems. In Computer Aided Verification - 28th International Conference (CAV), LNCS 9780, pages 251-269, 2016. [ bib ]

R. Alur, M. Faella, S. Kannan, and N. Singhania. Hedging Bets in Markov Decision Processes. In 25th EACSL Annual Conference on Computer Science Logic (CSL), LIPIcs 62, pages 29:1-29:20, 2016. [ bib ]

R. Alur, D. Fisman, and M. Raghothaman. Regular Programming for Quantitative Properties of Data Streams. In Programming Languages and Systems - 25th European Symposium on Programming (ESOP), LNCS 9632, pages 15-40, 2016. [ bib ]

R. Alur, S. Moarref, and U. Topcu. Compositional Synthesis with Parametric Reactive Controllers. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (HSCC), pages 215-224, 2016. [ bib ]

R. Alur and D. Fisman. Colored Nested Words. In Language and Automata Theory and Applications - 10th International Conference (LATA), LNCS 9618, pages 143-155, 2016. [ bib ]

Benjamin C. Pierce. A Deep Specification for Dropbox, November 2015. Keynote address at Clojure/conj. [ bib | slides ]

Benjamin C. Pierce. The Age of Deep Specification, May 2015. Honorary doctorate address at Chalmers University. [ bib | slides ]

Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, 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 ]

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 ]

Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational Property-Based Testing. In International Conference on Interactive Theorem Proving (ITP), 2015. [ bib ]

Udit Dhawan, Catalin Hritcu, 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 ]

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 ]

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, 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 ]

Justin Hsu. Death, taxes, and formal verification (Abstract). In Summit on Advances in Programming Languages (SNAPL), Asilomar, California, 2015. [ bib | slides | .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 ]

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. [ 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 ]

Neelakantan R. Krishnaswami, Jennifer Paykin, and Steve Zdancewic. Curry-Howard for GUIs. In POPL Off the Beaten Track (OBT), 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 ]

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 ]

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 ]

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 ]

Ravi Mangal, Xin Zhang, Aditya Nori, and Mayur Naik. Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances. In International Conference on Theory and Applications of Satisfiability Testing (SAT), 2015. [ bib | slides | .pdf ]

Ravi Mangal, Xin Zhang, Aditya Nori, and Mayur Naik. A User-Guided Approach to Program Analysis. In Symposium on Foundations of Software Engineering (FSE), 2015. [ bib | slides | .pdf ]

Jongse Park, Hadi Esmaeilzadeh, Xin Zhang, Mayur Naik, and William Harris. FlexJava: Language Support for Safe and Modular Approximate Programming. In Symposium on Foundations of Software Engineering (FSE), 2015. [ bib | slides | .pdf ]

Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, and Hongseok Yang. Modularity in Lattices: A Case Study on the Correspondence between Top-Down and Bottom-Up Analysis. In Static Analysis Symposium (SAS), 2015. [ bib | .pdf ]

L. D'Antoni, D. Kini, R. Alur, S. Gulwani, M. Viswanathan, and B. Hartmann. How Can Automatic Feedback Help Students Construct Automata? ACM Trans. Computer-Human Inter., 22(2):9:1-9:24, 2015. [ bib ]

R. Alur, L. D'Antoni, and M. Raghothaman. DReX: A declarative language for efficiently evaluating regular string tranformations. In Proceedings of the 42nd ACM Symposium on Principles of Programming Languages (POPL), pages 125-137, 2015. [ bib ]

R. Alur, T. A. Henzinger, and M. Y. Vardi. Theory in practice for system design and verification. SIGLOG News, 2(1):46-51, 2015. [ bib ]

L. D'Antoni, M. Weaver, A. Weinert, and R. Alur. Automata Tutor and what we learned from building an online teaching tool. Bulletin of the EATCS, 117, 2015. [ bib ]

R. Alur, P. Cerny, and A. Radhakrishna. Synthesis Through Unification. In Computer Aided Verification - 27th International Conference (CAV), LNCS 9207, pages 163-179, 2015. [ bib ]

R. Alur, M. Raghothaman, C. Stergiou, S. Tripakis, and A. Udupa. Automatic Completion of Distributed Protocols with Symmetry. In Computer Aided Verification - 27th International Conference (CAV), LNCS 9207, pages 395-412, 2015. [ bib ]

R. Alur, S. Moarref, and U. Topcu. Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference (TACAS), LNCS 9035, pages 501-516, 2015. [ bib ]

R. Alur, D. Fisman, R. Singh, and A. Solar-Lezama. Results and Analysis of SyGuS-Comp'15. In Proceedings Fourth Workshop on Synthesis (SYNT), EPTCS 202, pages 3-26, 2015. [ bib ]

Y. Yuan, D. Lin, R. Alur, and B. T. Loo. Scenario-based programming for SDN policies. In 11th Conference on Emerging Networking Experiments and Technologies (CoNEXT), 2015. [ bib ]

R. Alur. Principles of Cyber-Physical Systems. MIT Press, 2015. [ bib ]

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 ]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe Zero-Cost Coercions for Haskell. In The 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 189-202, September 2014. [ bib | .pdf ]

Benjamin C. Pierce. Programmable Hardware Support for Ubiquitous Micro-Policy Enforcement, May 2014. Talk at High-Confidence Software Systems. [ bib | slides ]

Benjamin C. Pierce. Interview with Luke Muehlhauser on Clean-Slate Security Architectures for Machine Intelligence Research Institute blog, May 2014. [ bib ]

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 ]

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 ]

Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, 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 to appear in Journal of Computer Security, Special Issue on Verified Information Flow Security, 2016. [ bib | full version | .pdf ]

Benjamin C. Pierce. Principles, Meet Practice: An Early Retrospective on SAFE, January 2014. Talk at Principles in Practice Workshop (PiP). [ bib | slides ]

Daniel Wagner. Symmetric Edit Lenses: A New Foundation for Bidirectional Languages. PhD thesis, University of Pennsylvania, 2014. [ bib | .pdf ]

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 ]

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 ]

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 ]

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 ]

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 ]

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining Proofs and Programs in a Dependently Typed Language. In POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 33-45, San Diego, CA, USA, 2014. [ bib | .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 ]

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 ]

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 ]

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. Technical report, University of Pennsylvania, 2014. [ bib | .pdf ]

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 ]

Cong Shi, Karim Habak, Pranesh Pandurangan, Mostafa Ammar, Mayur Naik, and Ellen Zegura. COSMOS: Computation Offloading as a Service for Mobile Devices. In Symposium on Mobile Ad Hoc Networking and Computing (MobiHoc), 2014. [ bib | .pdf ]

Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. On Abstraction Refinement for Program Analyses in Datalog. In Conference on Programming Language Design and Implementation (PLDI), 2014. [ bib | slides | .pdf ]

Xin Zhang, Ravi Mangal, Mayur Naik, and Hongseok Yang. Hybrid Top-Down and Bottom-Up Interprocedural Analysis. In Conference on Programming Language Design and Implementation (PLDI), 2014. [ bib | slides | .pdf ]

Ravi Mangal, Mayur Naik, and Hongseok Yang. A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join. In European Symposium on Programming (ESOP), 2014. [ bib | slides | .pdf ]

R. Alur, A. Freilich, and M. Raghothaman. Regular combinators for string transformations. In Proceedings of the 29th ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 9:1-9:10, 2014. [ bib ]

Z. Jiang, M. Pajic, R. Alur, and R. Mangharam. Closed-loop verification of medical devices with model abstraction and refinement. STTT, 16(2):191-213, 2014. [ bib ]

L. D'Antoni and R. Alur. Symbolic Visibly Pushdown Automata. In Computer Aided Verification - 26th International Conference (CAV), LNCS 8559, pages 209-225, 2014. [ bib ]

R. Alur and N. Singhania. Precise piecewise affine models from input-output data. In ACM International Conference on Embedded Software (EMSOFT), pages 3:1-3:10, 2014. [ bib ]

Y. Yuan, R. Alur, and B. T. Loo. NetEgg: Programming Network Policies by Examples. In Proceedings of the 13th ACM Workshop on Hot Topics in Networks (HotNets), pages 20:1-20:7, 2014. [ bib ]

R. Alur, M. M. K. Martin, M. Raghothaman, C. Stergiou, S. Tripakis, and A. Udupa. Synthesizing Finite-State Protocols from Scenarios and Requirements. In Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference (HVC), LNCS 8855, pages 75-91, 2014. [ bib ]

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 ]

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 ]

Catalin Hritcu, 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 ]

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, pages 275-286, Boston, MA, September 2013. [ bib | .pdf ]

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 ]

Benjamin C. Pierce. The SAFE Machine: An Architecture for Pervasive Information Flow, June 2013. Invited talk at Computer Security Foundations Symposium (CSF). [ bib | slides ]

Catalin Hritcu, 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 ]

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 ]

Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Edit languages for information trees. In Second International Workshop on Bidirectional Transformations (BX), April 2013. [ bib ]

Zhengjiang Hu, Shin-Cheng Mu, and Stephanie Weirich. Advanced programming techniques for construction of robust, generic and evolutionary programs, March 2013. [ bib | http ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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, MAR 2013. [ bib | .pdf ]

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 ]

Aravind Machiry, Rohan Tahiliani, and Mayur Naik. Dynodroid: An Input Generation System for Android Apps. In Symposium on Foundations of Software Engineering (FSE), 2013. [ bib | slides | .pdf ]

Yongin Kwon, Sangmin Lee, Hayoon Yi, Donghyun Kwon, Seungjun Yang, Byung-Gon Chun, Ling Huang, Petros Maniatis, Mayur Naik, and Yunheung Paek. Mantis: Automatic Performance Prediction for Smartphone Applications. In USENIX Annual Technical Conference (ATC), 2013. [ bib | slides | .pdf ]

Xin Zhang, Mayur Naik, and Hongseok Yang. Finding Optimum Abstractions in Parametric Dataflow Analysis. In Conference on Programming Language Design and Implementation (PLDI), 2013. [ bib | slides | .pdf ]

R. Alur, R. Bodík, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), pages 1-17, 2013. [ bib ]

R. Alur, S. Moarref, and U. Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. In Formal Methods in Computer-Aided Design (FMCAD), pages 26-33, 2013. [ bib ]

J. Thakkar, A. Kanade, and R. Alur. Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels. In Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference (FMOODS/FORTE), LNCS 7892, pages 209-224, 2013. [ bib ]

R. Alur, V. Forejt, S. Moarref, and A. Trivedi. Safe schedulability of bounded-rate multi-mode systems. In Proceedings of the 16th international conference on Hybrid systems: computation and control (HSCC), pages 243-252, 2013. [ bib ]

R. Alur, L. D'Antoni, J. V. Deshmukh, M. Raghothaman, and Y. Yuan. Regular Functions and Cost Register Automata. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 13-22, 2013. [ bib ]

A. Udupa, A. Raghavan, J.V. Deshmukh, S. Mador-Haim, M.M.K. Martin, and R. Alur. TRANSIT: specifying protocols with concolic snippets. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 287-296, 2013. [ bib ]

R. Alur and M. Raghothaman. Decision problems for additive regular functions. In Automata, Languages, and Programming - 40th ICALP, Part II, LNCS 7966, pages 37-48, 2013. [ bib ]

R. Alur, A. Durand-Gasselin, and A. Trivedi. From Monadic Second-Order Definable String Transformations to Transducers. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 458-467, 2013. [ bib ]

R. Alur, L. D'Antoni, S. Gulwani, D. Kini, and M. Viswanathan. Automated Grading of DFA Constructions. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI), pages 1976-1982, 2013. [ bib ]

R. Alur, S. Kannan, K. Tian, and Y. Yuan. On the Complexity of Shortest Path Problems on Discounted Cost Graphs. In Language and Automata Theory and Applications - 7th International Conference (LATA), LNCS 7810, pages 44-55, 2013. [ bib ]

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, Catalin Hritcu, 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 ]

Benjamin C. Pierce. Linguistic Foundations for Bidirectional Transformations, May 2012. Invited tutorial at Principles of Database Systems (PODS). [ bib | slides ]

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 talk given at FLOPS 2012. [ bib | slides ]

Benjamin C. Pierce. Types à la Milner, April 2012. Invited talk at Milner Symposium. [ bib | slides ]

Benjamin C. Pierce. Types à la Milner, April 2012. Talk at Philly Emerging Technologies Conference. [ bib ]

Kathleen Fisher, Ronald Garcia, and Stephanie Weirich. Nourishing the future of the field: the programming language mentoring workshop 2012, April 2012. [ bib | DOI ]

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 ]

Benjamin C. Pierce and editors Stephanie Weirich. Special Issue on the POPLMark Challenge. J. Autom. Reasoning, 49(3), 2012. [ bib ]

Benjamin C. Pierce. Types, January 2012. Invited talk at Programming Languages Mentoring Workshop. [ bib | slides ]

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 and Stephanie Weirich. Preface, 2012. [ bib ]

Umut A. Acar, James Cheney, and Stephanie Weirich. Editorial - Special issue dedicated to ICFP 2010, 2012. [ bib ]

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 ]

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 ]

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 ]

Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhaes. Giving Haskell A Promotion. In Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '12), pages 53-66, 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 ]

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 ]

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, 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 ]

Saswat Anand, Mayur Naik, Hongseok Yang, and Mary Jean Harrold. Automated Concolic Testing of Smartphone Apps. In Symposium on Foundations of Software Engineering (FSE), 2012. [ bib | slides | .pdf ]

Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv. Abstractions from Tests. In Symposium on Principles of Programming Languages (POPL), 2012. [ bib | slides | .pdf ]

T. Nghiem, G. J. Pappas, R. Alur, and A. Girard. Time-Triggered Implementations of Dynamic Controllers. ACM Trans. Embedded Comput. Syst., 11(S2):58, 2012. [ bib ]

R. Alur, P. Cerny, and S. Weinstein. Algorithmic analysis of array-accessing programs. ACM Trans. Comput. Log., 13(3):27, 2012. [ bib ]

S. Mador-Haim, L. Maranget, S. Sarkar, K. Memarian, J. Alglave, S. Owens, R. Alur, M. M. K. Martin, P. Sewell, and D. Williams. An Axiomatic Memory Model for POWER Multiprocessors. In Computer Aided Verification - 24th International Conference (CAV), LNCS 7358, pages 495-512, 2012. [ bib ]

R. Alur, A. Trivedi, and D. Wojtczak. Optimal scheduling for constant-rate multi-mode systems. In Hybrid Systems: Computation and Control (HSCC), pages 75-84, 2012. [ bib ]

R. Alur, E. Filiot, and A. Trivedi. Regular Transformations of Infinite Strings. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 65-74, 2012. [ bib ]

Z. Jiang, M. Pajic, S. Moarref, R. Alur, and R. Mangharam. Modeling and Verification of a Dual Chamber Implantable Pacemaker. In Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference (TACAS), LNCS 7214, pages 188-203, 2012. [ bib ]

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 ]

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 ]

Joao 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 ]

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 ]

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, 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 ]

R. Alur, A. D'Innocenzo, K. H. Johansson, G. J. Pappas, and G. Weiss. Compositional Modeling and Analysis of Multi-Hop Control Networks. IEEE Trans. Automat. Contr., 56(10):2345-2357, 2011. [ bib ]

R. Alur, S. Chaudhuri, and P. Madhusudan. Software model checking using languages of nested trees. ACM Trans. Program. Lang. Syst., 33(5):15, 2011. [ bib ]

R. Alur and A. Trivedi. Relating average and discounted costs for quantitative analysis of timed systems. In Proceedings of the 11th ACM International Conference on Embedded Software (EMSOFT), pages 165-174, 2011. [ bib ]

R. Alur. Formal verification of hybrid systems. In Proceedings of the 11th ACM International Conference on Embedded Software (EMSOFT), pages 273-278, 2011. [ bib ]

S. Mador-Haim, R. Alur, and M. M. K. Martin. Litmus tests for comparing memory consistency models: how long do they need to be? In Proceedings of the 48th ACM Design Automation Conference (DAC), pages 504-509, 2011. [ bib ]

R. Alur and P. Cerny. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 599-610, 2011. [ bib ]

R. Alur and J. V. Deshmukh. Nondeterministic Streaming String Transducers. In Automata, Languages and Programming - 38th International Colloquium, (ICALP), LNCS 6756, pages 1-20, 2011. [ bib ]

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 ]

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 ]

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 ]

Stephanie Weirich, editor. International Conference on Functional Programming. ACM Press, September 2010. [ bib ]

Stephanie Weirich. ICFP 2010 PC Chair's Report, September 2010. [ bib ]

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 ]

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 ]

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 ]

Brian Aydemir and Stephanie Weirich. LNgen: Tool Support for Locally Nameless Representations. Technical Report MS-CIS-10-24, Computer and Information Science, University of Pennsylvania, June 2010. [ bib | http ]

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 ]

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, 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 ]

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 ]

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 ]

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 ]

Jianzhou Zhao, Qi Zhang, and Steve Zdancewic. Relational Parametricity for Polymorphic Linear Lambda Calculus (Extended TR). 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 ]

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 ]

Peng Li and Steve Zdancewic. Arrows for Secure Information Flow. Theoretical Computer Science, 411(19):1974-1994, 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 ]

S. Mador-Haim, R. Alur, and M. M. K. Martin. Generating Litmus Tests for Contrasting Memory Consistency Models. In Computer Aided Verification, 22nd International Conference (CAV), LNCS 6174, pages 273-287, 2010. [ bib ]

P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur. Model Checking of Linearizability of Concurrent List Implementations. In Computer Aided Verification, 22nd International Conference (CAV), LNCS 6174, pages 465-479, 2010. [ bib ]

R. Alur and P. Cerny. Expressiveness of streaming string transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LIPIcs 8, pages 1-12, 2010. [ bib ]

R. Alur and S. Chaudhuri. Temporal Reasoning for Procedural Programs. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference (VMCAI), LNCS 5944, pages 45-60, 2010. [ bib ]

A. Kanade, R. Alur, S. K. Rajamani, and G. Ramalingam. Representation dependence testing using program inversion. In Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pages 277-286, 2010. [ bib ]

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, editor. Haskell Symposium. ACM Press, August 2009. [ bib ]

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 ]

Véronique Benzaken, Giuseppe Castagna, Haruo Hosoya, Benjamin C. Pierce, and Stijn Vansummeren. XML Typechecking. In Encyclopedia of Database Systems. Springer, 2009. [ bib ]

Benjamin C. Pierce, editor. Principles of Programming Languages (POPL). ACM Press, 2009. [ bib ]

Benjamin C. Pierce. POPL 2009 PC Chair's Report, January 2009. [ bib | slides ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

R. Alur and P. Madhusudan. Adding nesting structure to words. J. ACM, 56(3), 2009. [ bib ]

A. D'Innocenzo, G. Weiss, R. Alur, A. J. Isaksson, K. H. Johansson, and G. J. Pappas. Scalable scheduling algorithms for wireless networked control systems. In IEEE Conference on Automation Science and Engineering (CASE), pages 409-414, 2009. [ bib ]

P. Cerny and R. Alur. Automated Analysis of Java Methods for Confidentiality. In Computer Aided Verification, 21st International Conference (CAV), LNCS 5643, pages 173-187, 2009. [ bib ]

A. Kanade, R. Alur, F. Ivancic, S. Ramesh, S. Sankaranarayanan, and K. C. Shashidhar. Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. In Computer Aided Verification, 21st International Conference (CAV), LNCS 5643, pages 430-445, 2009. [ bib ]

G. Weiss, A. D'Innocenzo, R. Alur, K. H. Johansson, and G. J. Pappas. Robust stability of multi-hop control networks. In Proceedings of the 48th IEEE Conference on Decision and Control (CDC), pages 2210-2215, 2009. [ bib ]

R. Alur, P. Cerny, and S. Weinstein. Algorithmic Analysis of Array-Accessing Programs. In Computer Science Logic, 23rd international Workshop (CSL), LNCS 5771, pages 86-101, 2009. [ bib ]

R. Alur, A. Degorre, O. Maler, and G. Weiss. On Omega-Languages Defined by Mean-Payoff Conditions. In Foundations of Software Science and Computational Structures, 12th International Conference (FOSSACS), LNCS 5504, pages 333-347, 2009. [ bib ]

G. Weiss, S. Fischmeister, M. Anand, and R. Alur. Specification and Analysis of Network Resource Requirements of Control Systems. In Hybrid Systems: Computation and Control, 12th International Conference (HSCC), LNCS 5469, pages 381-395, 2009. [ bib ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Stephen Tse and Steve Zdancewic. Concise Concrete Syntax. Technical Report MS-CIS-08-11, 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 ]

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 ]

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 ]

W. Nam, P. Madhusudan, and R. Alur. Automatic symbolic compositional verification by learning assumptions. Formal Methods in System Design, 32(3):207-234, 2008. [ bib ]

R. Alur, M. Arenas, P. Barceló, K. Etessami, N. Immerman, and L. Libkin. First-Order and Temporal Logics for Nested Words. Logical Methods in Computer Science, 4(4), 2008. [ bib ]

R. Alur, A. Kanade, and G. Weiss. Ranking Automata and Games for Prioritized Requirements. In Computer Aided Verification, 20th International Conference (CAV), LNCS 5123, pages 240-253, 2008. [ bib ]

R. Alur, A. Kanade, S. Ramesh, and K. C. Shashidhar. Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In Proceedings of the 8th ACM & IEEE International conference on Embedded software (EMSOFT), pages 89-98, 2008. [ bib ]

R. Alur and G. Weiss. RTComposer: a framework for real-time components with scheduling interfaces. In Proceedings of the 8th ACM & IEEE International conference on Embedded software (EMSOFT), pages 159-168, 2008. [ bib ]

R. Alur. Model Checking: From Tools to Theory. In 25 Years of Model Checking - History, Achievements, Perspectives, LNCS 5000, pages 89-106, 2008. [ bib ]

R. Alur and G. Weiss. Regular Specifications of Resource Requirements for Embedded Control Software. In Proceedings of the 14th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pages 159-168, 2008. [ bib ]

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 ]

Benjamin C. Pierce. Adventures in Bi-Directional Programming, December 2007. FSTTCS invited talk. [ bib | slides ]

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. 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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

R. Alur and A. Chandrashekharapuram. Dispatch sequences for embedded control models. J. Comput. Syst. Sci., 73(2):156-170, 2007. [ bib ]

M. Bernadsky and R. Alur. Symbolic Analysis for GSMP Models with One Stateful Clock. In Hybrid Systems: Computation and Control, 10th International Workshop (HSCC), LNCS 4416, pages 90-103, 2007. [ bib ]

G. Weiss and R. Alur. Automata Based Interfaces for Control and Scheduling. In Hybrid Systems: Computation and Control, 10th International Workshop (HSCC), LNCS 4416, pages 601-613, 2007. [ bib ]

R. Alur, M. Arenas, P. Barceló, K. Etessami, N. Immerman, and L. Libkin. First-Order and Temporal Logics for Nested Words. In 22nd IEEE Symposium on Logic in Computer Science (LICS), pages 151-160, 2007. [ bib ]

S. Burckhardt, R. Alur, and M. M. K. Martin. CheckFence: checking consistency of concurrent data types on relaxed memory models. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 12-21, 2007. [ bib ]

R. Alur, P. Cerny, and S. Chaudhuri. Model Checking on Trees with Path Equivalences. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference (TACAS), LNCS 4424, pages 664-678, 2007. [ bib ]

Rajeev Alur. Marrying words and trees. In Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS), pages 233-242, 2007. [ bib ]

S. Chaudhuri and R. Alur. Instrumenting C Programs with Nested Word Monitors. In Model Checking Software, 14th International SPIN Workshop, LNCS 4595, pages 279-283, 2007. [ bib ]

Stephanie Weirich. Type-Safe Run-time Polytypic Programming. Journal of Functional Programming, 16(10):681-710, November 2006. [ bib | .pdf ]

Andrew J. Kennedy and Benjamin C. Pierce. On Decidability of Nominal Subtyping with Variance, September 2006. FOOL-WOOD '07. [ bib | short version ]

Stephanie Weirich. RepLib: A library for derivable type classes. In Haskell Workshop, pages 1-12, 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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Rajeev Alur, Pavol Cerny, 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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Benjamin C. Pierce. Fancy Types for XML: Friend or Foe?, April 2005. Talk at LINKS workshop, April 2005. [ bib | slides ]

Benjamin C. Pierce. Harmony: The Art of Reconciliation, April 2005. Invited talk at Trusted Global Computing conference, April 2005. [ bib | slides ]

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 ]

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 ]

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 ]

Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and Alan Schmitt. The Xtatic Compiler and Runtime System, 2005. [ bib | source code ]

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 ]

Benjamin C. Pierce, editor. Advanced Topics in Types and Programming Languages. MIT Press, 2005. [ bib | home page ]

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 ]

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 ]

Benjamin C. Pierce, editor. International Conference on Functional Programming (ICFP). ACM Press, 2005. [ bib ]

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 ]

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 ]

Peng Li and Steve Zdancewic. Unifying Confidentiality and Integrity in Downgrading Policies. In Proc. of Foundations of Computer Security Workshop (FCS), 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. 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 ]

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 ]

Stephanie Weirich. Type-Safe Cast. Journal of Functional Programming, 14(6):681-695, November 2004. [ bib | http ]

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 ]

Vladimir Gapeyev and Benjamin C. Pierce. Paths into Patterns. Technical Report MS-CIS-04-25, University of Pennsylvania, October 2004. [ bib | tech report ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Stephen Tse and Steve Zdancewic. Translating Dependency into Parametricity. Technical Report MIS-CIS-04-01, University of Pennsylvania, 2004. [ bib | .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 ]

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 ]

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 ]

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 ]

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 ]

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 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 ]

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 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 ]

Benjamin C. Pierce. Types and Programming Languages: The Next Generation, 2003. Invited tutorial at Logic in Computer Science (LICS). [ bib | slides ]

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 ]

Trevor Jim, Benjamin C. Pierce, and Jérôme Vouillon. How to Build a File Synchronizer. Manuscript, 2003. [ bib ]

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 ]

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 ]

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 ]

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 ]

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. Manuscript; available at http://www.cis.upenn.edu/~bcpierce/papers/lenses.pdf, 2003. [ bib ]

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 ]

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 ]

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 ]

Stephanie Weirich. Programming With Types. PhD thesis, Cornell University, August 2002. [ bib | .ps | .pdf ]

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 ]

Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. [ bib | errata | home page ]

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 ]

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, 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 ]

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 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 ]

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 ]

Benjamin C. Pierce. Global Computing: Some Questions for FOOLs, 2001. Invited talk at FOOL workshop. [ bib | slides ]

Benjamin C. Pierce. File Synchronization: Theory and Practice, 2001. [ bib | slides ]

Benjamin C. Pierce. Unison: A file synchronizer and its specification, 2001. Invited talk at Theoretical Aspects of Computer Software (TACS), Sendai, Japan. [ bib | slides ]

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 ]

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 ]

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 ]

Benjamin C. Pierce and Jérôme Vouillon. Unison: A File Synchronizer and its Specification. Manuscript, 2001. [ bib ]

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 ]

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 ]

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 ]

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 ]

Benjamin C. Pierce. Module Systems: A Guide for the Perplexed, September 2000. Invited talk at ICFP, Montreal. [ bib ]

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 Pierce and Eijiro Sumii. Relating Cryptography and Polymorphism, July 2000. Some parts superseded by [330] (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. Chaining, Referral, Subscription, Leasing: New Mechanisms in Distributed Query Optimization, February 2000. [ bib ]

Arnaud Sahuguet, Benjamin Pierce, and Val Tannen. Distributed Query Optimization: Can Mobile Agents Help?, February 2000. [ bib ]

Benjamin C. Pierce. Advanced Module Systems: A Guide for the Perplexed, 2000. Invited tutorial at International Conference on Functional Programming (ICFP). [ bib | slides ]

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 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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

Benjamin C. Pierce. Type Systems for Concurrent Calculi, September 1998. Invited tutorial at CONCUR, Nice, France. [ bib ]

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 ]

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 ]

S. Balasubramaniam and Benjamin C. Pierce. File Synchronization. Technical Report 507, Computer Science Department, Indiana University, April 1998. [ bib ]

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 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 ]

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. Type Systems for Concurrent Calculi, 1998. Invited tutorial at CONCUR. [ bib | slides ]

Benjamin C. Pierce, Trevor Jim Sundar Balasubramaniam, Insup Lee, and Insik Shin. Snc: a file synchronizer, 1998. (Superseded by Unison.). [ bib ]

Haruo Hosoya, Benjamin C. Pierce, and David N. Turner. Datatypes and Subtyping. Manuscript, 1998. [ bib | .ps ]

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 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 ]

Benjamin C. Pierce. Bounded Quantification with Bottom. Technical Report 492, Computer Science Department, Indiana University, 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 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 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. Pict Language Definition. Available electronically, 1997. [ bib ]

Benjamin C. Pierce and David N. Turner. Pict Libraries Manual. 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. Programming in the Pi-Calculus: A Tutorial Introduction to Pict. Available electronically, 1997. [ bib ]

Benjamin C. Pierce. Review of A Theory of Objects, by Abadi and Cardelli. The Computer Journal, 40(5):297-298, 1997. [ bib | .ps ]

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. Even simpler type-theoretic foundations for OOP. Manuscript (circulated electronically), March 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. Types. Lecture notes for an undergraduate course at Cambridge University, February 1996. [ 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 ]

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 ]

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 ]

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 ]

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 ]

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. Using Types to Compare Objects and ADTs, October 1995. Invited lecture at Horizon Day, Indiana University. [ bib ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 ]

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 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 ]

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. Woggles from Oz: Writing Interactive Fiction. Leonardo: Journal of the International Society for the Arts, Sciences, and Technology, 1994. Expanded version available electronically. [ 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, 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. Mutable Objects. Draft report; available electronically, June 1993. [ bib | .ps ]

Benjamin C. Pierce. A Model of Delegation Based on Existential Types. Available electronically, April 1993. [ 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 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 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. Typage des Traits Orientés-Objets, February 1993. Invited lecture at Journeés Francophones des Langages Applicatifs, Annecy, France. [ bib ]

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 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. F-Omega-Sub: a polymorphic λ-calculus with higher-order subtyping and object-oriented extensions, 1993. [ bib ]

Benjamin C. Pierce and Robert Pollack. Higher-Order Subtyping. Unpublished manuscript, August 1992. [ bib ]

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 ]

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 ]

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 ]

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. Basic Category Theory for Computer Scientists. MIT Press, 1991. [ bib ]

Benjamin C. Pierce. Fmeet: a polymorphic λ-calculus with intersection types, 1991. [ 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. 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. Bounded Quantification and Intersection Types. Thesis proposal (unpublished), 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 ]

R. Alur and L. D'Antoni. Streaming Tree Transducers. In Automata, Languages, and Programming - 39th International Colloquium, ICALP Part II, LNCS 7392, pages 42-53. [ bib ]

Last modified: Tuesday, 24-Jan-2017 09:34:32 EST

Copyright Information

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Valid XHTML 1.1! Valid CSS!