The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.
The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.
Wed 10 Jan Times are displayed in time zone: Tijuana, Baja California change
08:30 - 10:00: Awards & Keynote-IResearch Papers at Bunker Hill / Watercourt Chair(s): Ranjit JhalaUniversity of California, San Diego | |||
08:30 - 08:35 Day opening | Welcome to POPL 2018 Research Papers | ||
08:35 - 08:45 Awards | SIGPLAN Awards Research Papers Satnam SinghX, the moonshot factory | ||
08:45 - 09:45 Talk | Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can) Research Papers Derek DreyerMPI-SWS | ||
09:45 - 10:05 Talk | Lightning Overview - Day 1 Research Papers |
10:30 - 12:10: StringsResearch Papers at Bunker Hill Chair(s): Zachary TatlockUniversity of Washington, Seattle | |||
10:30 - 10:55 Talk | Synthesizing Bijective Lenses Research Papers Anders MiltnerPrinceton University, Kathleen FisherTufts University, Benjamin C. PierceUniversity of Pennsylvania, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania | ||
10:55 - 11:20 Talk | WebRelate: Integrating Web Data with Spreadsheets using Examples Research Papers | ||
11:20 - 11:45 Talk | What's Decidable About String Constraints with ReplaceAll Function? Research Papers Taolue ChenBirkbeck, University of London, Yan ChenState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Zhilin WuState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences | ||
11:45 - 12:10 Talk | String Constraints with Concatenation and Transducers Solved Efficiently Research Papers Lukáš HolíkBrno University of Technology, Anthony Widjaja LinOxford University, Petr JankůBrno University of Technology, Philipp RuemmerUppsala University, Tomáš VojnarBrno University of Technology |
10:30 - 12:10: Types and EffectsResearch Papers at Watercourt Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge | |||
10:30 - 10:55 Talk | Linear Haskell: practical linearity in a higher-order polymorphic language Research Papers Jean-Philippe BernardyUniversity of Gothenburg, Mathieu BoespflugTweag I/O, Ryan R. NewtonIndiana University, Simon Peyton JonesMicrosoft Research, Arnaud SpiwackTweag I/O Pre-print File Attached | ||
10:55 - 11:20 Talk | Polyadic Approximations, Fibrations and Intersection Types Research Papers | ||
11:20 - 11:45 Talk | Handling fibred algebraic effects Research Papers Danel AhmanInria Paris | ||
11:45 - 12:10 Talk | Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Research Papers Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław |
12:10 - 13:40 Lunch | Wednesday Lunch Research Papers |
13:40 - 14:05 Talk | Automated Lemma Synthesis in Symbolic-Heap Separation Logic Research Papers Quang-Trung TaNational University of Singapore, Ton Chanh LeNational University of Singapore, Siau-Cheng KhooNational University of Singapore, Wei-Ngan ChinNational University of Singapore | ||
14:05 - 14:30 Talk | Foundations for Natural Proofs and Quantifier Instantiation Research Papers Christof LödingRWTH Aachen University, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Lucas PeñaUniversity of Illinois at Urbana-Champaign | ||
14:30 - 14:55 Talk | Higher-Order Constrained Horn Clauses for Verification Research Papers Toby Cathcart BurnUniversity of Oxford, C.-H. Luke OngUniversity of Oxford, Steven RamsayUniversity of Bristol | ||
14:55 - 15:20 Talk | Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs Research Papers Hiroshi UnnoUniversity of Tsukuba, Yuki SatakeUniversity of Tsukuba, Tachio TerauchiWaseda University |
13:40 - 15:20: Interpretation and EvaluationResearch Papers at Watercourt Chair(s): Atsushi IgarashiKyoto University, Japan | |||
13:40 - 14:05 Talk | Unifying Analytic and Statically-Typed Quasiquotes Research Papers Lionel ParreauxEPFL, Antoine VoizardUniversity of Pennsylvannia, Amir ShaikhhaEPFL, Christoph E. KochEPFL Pre-print | ||
14:05 - 14:30 Talk | Jones-Optimal Partial Evaluation by Specialization-Safe Normalization Research Papers | ||
14:30 - 14:55 Talk | Migrating Gradual Types Research Papers John Peter CamporaULL Lafayette, Sheng ChenUniversity of Louisiana at Lafayette, Martin ErwigOregon State University, Eric WalkingshawOregon State University | ||
14:55 - 15:20 Talk | Intrinsically-Typed Definitional Interpreters for Imperative Languages Research Papers Casper Bach PoulsenDelft University of Technology, Arjen RouvoetDelft University of Technology, Andrew TolmachPortland State University, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology DOI Pre-print |
15:50 - 17:30: Memory and ConcurrencyResearch Papers at Bunker Hill Chair(s): Azadeh FarzanUniversity of Toronto | |||
15:50 - 16:15 Talk | Effective Stateless Model Checking for C/C++ Concurrency Research Papers Michalis KokologiannakisNational Technical University of Athens, Greece, Ori LahavTel Aviv University, Israel, Konstantinos (Kostis) Sagonas, Viktor VafeiadisMPI-SWS, Germany | ||
16:15 - 16:40 Talk | Transactions in Relaxed Memory Architectures Research Papers Brijesh DongolBrunel University London, Radha JagadeesanDePaul University, James RielyDePaul University Link to publication DOI Pre-print Media Attached | ||
16:40 - 17:05 Talk | Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Research Papers Christopher PulteUniversity of Cambridge, Shaked FlurUniversity of Cambridge, Will DeaconARM Ltd., Jon FrenchUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, Peter SewellUniversity of Cambridge | ||
17:05 - 17:30 Talk | Progress of Concurrent Objects with Partial Methods Research Papers Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China |
15:50 - 17:30: TypesResearch Papers at Watercourt Chair(s): Thorsten AltenkirchUniversity of Nottingham | |||
15:50 - 16:15 Talk | A Principled approach to Ornamentation in ML Research Papers | ||
16:15 - 16:40 Talk | Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible Research Papers William J. BowmanNortheastern University, USA, Youyou CongOchanomizu University, Japan, Nick RiouxNortheastern University, USA, Amal AhmedNortheastern University, USA Link to publication DOI Pre-print | ||
16:40 - 17:05 Talk | Safety and Conservativity of Definitions in HOL and Isabelle/HOL Research Papers | ||
17:05 - 17:30 Talk | Univalent Higher Categories via Complete Semi-Segal Types Research Papers |
19:00 - 22:00 Dinner | POPL Banquet Research Papers |
Thu 11 Jan Times are displayed in time zone: Tijuana, Baja California change
08:30 - 10:00: Keynote-IIResearch Papers at Bunker Hill / Watercourt Chair(s): Andrew C. MyersCornell University | |||
08:30 - 09:30 Talk | Some Principles of Differential Programming Languages Research Papers Gordon PlotkinUniversity of Edinburgh, UK | ||
09:30 - 10:00 Talk | Lightning Overview - Day 2 Research Papers |
10:30 - 12:10: ConsistencyResearch Papers at Bunker Hill Chair(s): Xinyu FengUniversity of Science and Technology of China | |||
10:30 - 10:55 Talk | Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections Research Papers | ||
10:55 - 11:20 Talk | Reducing Liveness to Safety in First-Order Logic Research Papers Oded PadonTel Aviv University, Jochen HoenickeUniversität Freiburg, Giuliano LosaUniversity of California at Los Angeles, USA, Andreas PodelskiUniversity of Freiburg, Germany, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university | ||
11:20 - 11:45 Talk | Alone Together: Compositional Reasoning and Inference for Weak Isolation Research Papers Gowtham KakiPurdue University, Kartik NagarPurdue University, Mahsa NajafzadehPurdue University, Suresh JagannathanPurdue University | ||
11:45 - 12:10 Talk | Programming and Proving with Distributed Protocols Research Papers Ilya SergeyUniversity College London, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle DOI Pre-print |
10:30 - 12:10: Program Analysis IResearch Papers at Watercourt Chair(s): Tachio TerauchiWaseda University | |||
10:30 - 10:55 Talk | Inference of Static Semantics for Incomplete C Programs Research Papers Leandro T. C. MeloUFMG, Rodrigo Geraldo RibeiroUFOP, Marcus Rodrigues de AraújoUFMG, Fernando Magno Quintão PereiraUFMG Pre-print | ||
10:55 - 11:20 Talk | Optimal Dyck Reachability for Data-dependence and Alias Analysis Research Papers | ||
11:20 - 11:45 Talk | Data-centric Dynamic Partial Order Reduction Research Papers Marek ChalupaMasaryk University, Krishnendu ChatterjeeIST Austria, Andreas PavlogiannisIST Austria, Kapil VaidyaIIT Bombay, Nishant SinhaIBM Research | ||
11:45 - 12:10 Talk | Analytical Modeling of Cache Behavior for Affine Programs Research Papers Wenlei BaoOhio State University, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noël PouchetColorado State University, P. SadayappanOhio State University |
12:10 - 13:40 Lunch | Thursday Lunch Research Papers |
13:40 - 15:20: TerminationResearch Papers at Bunker Hill Chair(s): Constantin EneaUniversité Paris Diderot | |||
13:40 - 14:05 Talk | A new proof rule for almost-sure termination Research Papers Annabelle McIverMacquarie University, Carroll MorganUniversity of New South Wales; Data 61, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University | ||
14:05 - 14:30 Talk | Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Research Papers | ||
14:30 - 14:55 Talk | Algorithmic Analysis of Termination Problems for Quantum Programs Research Papers Yangjia LiInstitute of Software, Chinese Academy of Sciences, Mingsheng YingUniversity of Technology Sydney | ||
14:55 - 15:20 Talk | Monadic refinements for relational cost analysis Research Papers Ivan RadicekTU Vienna, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Florian ZulegerTU Vienna |
13:40 - 15:20: Outside the boxResearch Papers at Watercourt Chair(s): Lars BirkedalAarhus University | |||
13:40 - 14:05 Talk | Go with the Flow: Compositional Abstractions for Concurrent Data Structures Research Papers Siddharth KrishnaNew York University, Dennis ShashaNew York University, Thomas WiesNew York University | ||
14:05 - 14:30 Talk | Parametricity versus the Universal Type Research Papers | ||
14:30 - 14:55 Talk | Linearity in Higher-Order Recursion Schemes Research Papers Pierre ClairambaultCNRS & ENS Lyon, Charles GrelloisINRIA Sophia Antipolis & Aix-Marseille Université, Andrzej MurawskiUniversity of Oxford | ||
14:55 - 15:20 Talk | Symbolic Types for Lenient Symbolic Execution Research Papers Stephen ChangNortheastern University, Alex KnauthNortheastern University, Emina TorlakUniversity of Washington |
15:50 - 16:40: Language DesignResearch Papers at Bunker Hill Chair(s): Zachary TatlockUniversity of Washington, Seattle | |||
15:50 - 16:15 Talk | An Axiomatic Basis for Bidirectional Programming Research Papers Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Japan, Zhenjiang HuNational Institute of Informatics Link to publication DOI Pre-print Media Attached File Attached | ||
16:15 - 16:40 Talk | Simplicitly: Foundations and Applications of Implicit Function Types Research Papers Martin OderskyEPFL, Switzerland, Olivier BlanvillainEPFL, Fengyun LiuEPFL, Switzerland, Aggelos BiboudisEcole Polytechnique Federale de Lausanne, Heather MillerEcole Polytechnique Federale de Lausanne, Sandro StuckiEPFL |
15:50 - 16:40: Dependent TypesResearch Papers at Watercourt Chair(s): Karl CraryCarnegie Mellon University | |||
15:50 - 16:15 Talk | Up-to Techniques Using Sized Types Research Papers Nils Anders DanielssonUniversity of Gothenburg, Chalmers University of Technology | ||
16:15 - 16:40 Talk | Decidability of Conversion for Type Theory in Type Theory Research Papers Andreas AbelGothenburg University, Joakim ÖhmanIMDEA Software Institute, Andrea VezzosiChalmers University of Technology |
17:00 - 18:00: Business MeetingResearch Papers at Bunker Hill / Watercourt Chair(s): Andrew C. MyersCornell University, Ranjit JhalaUniversity of California, San Diego | |||
17:00 - 17:20 Talk | Chairs' Report Research Papers | ||
17:20 - 17:30 Talk | POPL 2019 Preview Research Papers | ||
17:30 - 18:00 Talk | SIGPLAN Town Hall Research Papers |
18:15 - 20:15 Other | POPL Poster Session Research Papers |
Fri 12 Jan Times are displayed in time zone: Tijuana, Baja California change
08:30 - 10:00: Keynote-IIIResearch Papers at Bunker Hill / Watercourt Chair(s): Andrew C. MyersCornell University | |||
08:30 - 09:30 Talk | Formal Methods and the Law Research Papers | ||
09:30 - 10:00 Talk | Lightning Overview - Day 3 Research Papers |
10:30 - 12:10: Testing and VerificationResearch Papers at Bunker Hill Chair(s): Santosh NagarakatteRutgers University, USA | |||
10:30 - 10:55 Talk | Generating Good Generators for Inductive Relations Research Papers Leonidas LampropoulosUniversity of Pennsylvania, Zoe ParaskevopoulouPrinceton University, Benjamin C. PierceUniversity of Pennsylvania | ||
10:55 - 11:20 Talk | Why is Random Testing Effective for Partition Tolerance Bugs? Research Papers | ||
11:20 - 11:45 Talk | On Automatically Proving the Correctness of math.h Implementations Research Papers | ||
11:45 - 12:10 Talk | Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Research Papers Shelly GrossmanTel Aviv University, Ittai AbrahamVMWare Research, Guy Golan-GuetaVMWare Research, Yan MichalevskyStanford University, Noam RinetzkyTel Aviv University, Mooly SagivTel Aviv University, Yoni ZoharTel Aviv University |
10:30 - 12:10: Dynamic LanguagesResearch Papers at Watercourt Chair(s): Jean YangCarnegie Mellon University | |||
10:30 - 10:55 Talk | Correctness of Speculative Optimizations with Dynamic Deoptimization Research Papers Olivier FlückigerNortheastern University, USA, Gabriel SchererNortheastern University, USA, Ming-Ho YeeNortheastern University, USA, Aviral GoelNortheastern University, Amal AhmedNortheastern University, USA, Jan VitekNortheastern University DOI Pre-print | ||
10:55 - 11:20 Talk | JaVerT: JavaScript Verification Toolchain Research Papers José Fragoso SantosImperial College London, Petar MaksimovićImperial College London, Daiva NaudžiūnienėImperial College London, Thomas WoodImperial College London, Philippa GardnerImperial College London | ||
11:20 - 11:45 Talk | Soft Contract Verification for Higher-order Stateful Programs Research Papers Phúc C. NguyễnUniversity of Maryland, Thomas GilrayUniversity of Maryland, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland | ||
11:45 - 12:10 Talk | Collapsing Towers of Interpreters Research Papers |
12:10 - 13:30 Lunch | Friday Lunch Research Papers |
13:30 - 13:40 Awards | SRC Awards Research Papers Benjamin DelawarePurdue University | ||
13:30 - 13:52 Talk | Refinement Reflection: Complete Verification with SMT Research Papers Niki VazouUniversity of Maryland, Anish TondwalkarUCSD, Vikraman Choudhury, Ryan ScottIndiana University, Ryan R. NewtonIndiana University, Philip WadlerUniversity of Edinburgh, UK, Ranjit JhalaUniversity of California, San Diego | ||
14:05 - 14:30 Talk | Non-Linear Reasoning For Invariant Synthesis Research Papers Zachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc. | ||
14:30 - 14:55 Talk | A Practical Construction for Decomposing Numerical Abstract Domains Research Papers | ||
14:55 - 15:20 Talk | Verifying Equivalence of Database-Driven Applications Research Papers Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu LahiriMicrosoft Research, William CookUniversity of Texas at Austin |
13:40 - 14:05 Talk | Proving expected sensitivity of probabilistic programs Research Papers Gilles BartheIMDEA Software Institute, Thomas EspitauUniversite Pierre et Marie Curie, Benjamin GregoireINRIA, Justin HsuUniversity College London, Pierre-Yves StrubEcole Polytechnique | ||
14:05 - 14:30 Talk | Synthesizing Coupling Proofs of Differential Privacy Research Papers | ||
14:30 - 14:55 Talk | Measurable cones and stable, measurable functions Research Papers Thomas EhrhardCNRS and University Paris Diderot, Michele PaganiUniversity Paris Diderot, Christine TassonUniversity Paris Diderot | ||
14:55 - 15:20 Talk | Denotational validation of higher-order Bayesian inference Research Papers Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Ohad KammarUniversity of Oxford, Matthijs VákárUniversity of Oxford, Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, Yufei CaiUniversity of Tuebingen, Klaus OstermannUniversity of Tuebingen, Sean K. MossUniversity of Cambridge, Chris HeunenUniversity of Edinburgh, Zoubin GhahramaniUniversity of Cambridge |
15:50 - 17:05: SynthesisResearch Papers at Bunker Hill Chair(s): Nadia PolikarpovaUniversity of California, San Diego | |||
15:50 - 16:15 Talk | Strategy Synthesis for Linear Arithmetic Games Research Papers | ||
16:15 - 16:40 Talk | Bonsai: Synthesis-Based Reasoning for Type Systems Research Papers | ||
16:40 - 17:05 Talk | Program Synthesis using Abstraction Refinement Research Papers |
15:50 - 17:05: Types for StateResearch Papers at Watercourt Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge | |||
15:50 - 16:15 Talk | A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST Research Papers Amin Timanyimec-Distrinet KU-Leuven, Leo StefanescoENS Lyon, Morten Krogh-JespersenAarhus University, Lars BirkedalAarhus University | ||
16:15 - 16:40 Talk | Recalling a Witness: Foundations and Applications of Monotonic State Research Papers Danel AhmanInria Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris and ENS Paris, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research Pre-print | ||
16:40 - 17:05 Talk | RustBelt: Securing the Foundations of the Rust Programming Language Research Papers Ralf JungMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology, Derek DreyerMPI-SWS |
Not scheduled yet
Not scheduled yet Other | Poster Session for POPL Papers Research Papers | ||
Not scheduled yet Lunch | Wed Lunch Research Papers | ||
Not scheduled yet Lunch | Lunch Research Papers |
Call for Papers
Scope
The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.
The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.
Evaluation criteria
The Program Committee will evaluate the technical contribution of each submission as well as its accessibility to both experts and the general POPL audience. All papers will be judged on significance, originality, relevance, correctness, and clarity.
Each paper should explain its contributions in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. Authors should strive to make their papers understandable to a broad audience. Advice on writing technical papers can be found on the SIGPLAN author information page.
Evaluation process
Authors will have a three-day period to respond to reviews, as indicated in the Important Dates table. Responses are optional. They must not be overly long and should not try to introduce new technical results. Reviewers will write a short reaction to these author responses.
As an experiment for POPL 2018, the program committee will discuss papers entirely electronically rather than at a physical programming committee meeting. This will avoid the time, cost and ecological impact of transporting an increasingly large committee to one point on the globe. Unlike in recent years, there will be no formal External Review Committee, though experts outside the committee will be consulted when their expertise is needed.
Reviews will be accompanied by a short summary of the reasons behind the committee's decision. It is the goal of the program committee to make it clear to the authors why each paper was or was not accepted.
For additional information about the reviewing process, see:
- Principles of POPL: a presentation of the underlying organizational and reviewing policies for POPL.
- Frequently asked questions about the reviewing and submission process, especially double-blind reviewing.
Submission guidelines
Prior to the paper submission deadline, the authors will upload their full
anonymized paper. Each paper should have no more than 24
26 27 + upto 4 extra (for $100 per page) pages of text, excluding
bibliography, using the new ACM Proceedings format. This format, new as of 2018, is
chosen for compatibility with PACMPL. It is a single-column page layout with a 10 pt
font, 12 pt line spacing, and wider margins than recent POPL page layouts. In this format, the main text block is 5.478 in (13.91 cm) wide and 7.884 in (20.03 cm) tall. A 26-page document contains about the same amount of text as a 12-page document in the format used in recent POPLs. Use of a denser format (e.g., smaller fonts or a larger text block) is grounds for summary rejection. Templates for the new ACM format for Microsoft Word and LaTeX (with the acmlarge acmsmall
option) can be found at the SIGPLAN author information page.
Submissions should be in PDF and printable on both US Letter and A4 paper. Papers may
be resubmitted to the submission site multiple times up until the deadline, but the
last version submitted before the deadline will be the version reviewed. Papers that
exceed the length requirement, that deviate from the expected format, or that are
submitted late will be rejected.
Deadlines expire at midnight anywhere on earth on the Important Dates displayed to the right.
Submitted papers must adhere to the SIGPLAN Republication Policy and the ACM Policy on Plagiarism. Concurrent submissions to other conferences, workshops, journals, or similar forums of publication are not allowed.
POPL 2018 will employ a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules:
- author names and institutions must be omitted, and
- references to authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”).
The purpose of this process is to help the PC and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult. In particular, important background references should not be omitted or anonymized. In addition, authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas. A document answering frequently asked questions should address many common concerns.
The submission itself is the object of review and so it should strive to convince the reader of at least the plausibility of reported results. Still, we encourage authors to provide any supplementary material that is required to support the claims made in the paper, such as detailed proofs, proof scripts, or experimental data. These materials must be uploaded at submission time, as a single pdf or a tarball, not via a URL. Two forms of supplementary material may be submitted.
- Anonymous supplementary material is available to the reviewers before they submit their first-draft reviews.
- Non-anonymous supplementary material is available to the reviewers after they have submitted their first-draft reviews and learned the identity of the authors.
Use the anonymous form if possible. Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper.
Artifact Evaluation
Authors of accepted papers will be invited to formally submit supporting materials to the Artifact Evaluation process. Artifact Evaluation is run by a separate committee whose task is to assess how the artifacts support the work described in the papers. This submission is voluntary and will not influence the final decision regarding the papers. Papers that go through the Artifact Evaluation process successfully will receive a seal of approval printed on the papers themselves. Authors of accepted papers are encouraged to make these materials publicly available upon publication of the proceedings, by including them as “source materials” in the ACM Digital Library.
PACMPL and Copyright
All papers accepted to POPL 2018 will also be published as part of the new ACM journal Proceedings of the ACM on Programming Languages (PACMPL), To conform with ACM requirements for journal publication, all POPL papers will be conditionally accepted; authors will be required to submit a short description of the changes made to the final version of the paper, including how the changes address any requirements imposed by the program committee. That the changes are sufficient will be confirmed by the original reviewers prior to acceptance to POPL.
As a Gold Open Access journal, PACMPL is committed to making peer-reviewed scientific research free of restrictions on both access and (re-)use. Authors are strongly encouraged to support libre open access by licensing their work with the Creative Commons Attribution 4.0 International (CC BY) license, which grants readers liberal (re-)use rights.
Authors of accepted papers will be required to choose one of the following publication rights:
- Author licenses the work with a Creative Commons license, retains copyright, and (implicitly) grants ACM non-exclusive permission to publish (suggested choice).
- Author retains copyright of the work and grants ACM a non-exclusive permission to publish license.
- Author retains copyright of the work and grants ACM an exclusive permssion to publish license.
- Author transfers copyright of the work to ACM.
These choices follow from ACM Copyright Policy and ACM Author Rights, corresponding to ACM's "author pays" option. While PACMPL may ask authors who have funding for open-access fees to voluntarily cover the article processing charge (currently, US$400), payment is not required or expected for publication. PACMPL and SIGPLAN continue to explore the best models for funding open access, focusing on approaches that are sustainable in the long-term while reducing short-term risk.
Publication and Presentation Requirements
Authors are required to give a short talk (roughly 25 minutes long) at the conference, according to the conference schedule. Papers may not be presented at the conference if they have not been published by ACM under one of the allowed copyright options.
POPL welcomes all authors, regardless of nationality. If authors are unable despite reasonable effort to obtain visas to travel to the conference, arrangements to enable remote participation will be made. In such cases, the general chair, Ranjit Jhala, should be contacted for guidance.
Final versions of accepted papers are allowed up to 24 26 pages excluding the
bibliography, using ACM Proceedings Format. In addition, up to four
additional pages may be purchased at US$100 per page. This additional amount
will be due at registration for the conference.
The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.
Accepted Papers
Submission and Reviewing FAQ
This FAQ is based on Mike Hicks' double-blind reviewing FAQ from POPL 2012, lightly-edited and slightly extended by David Walker for POPL 2015 and Andy Gordon for POPL 2017.
General
- Why are you using double-blind reviewing?
- Do you really think blinding actually works? I suspect reviewers can often guess who the authors are anyway.
- Couldn't blind submission create an injustice where a paper is inappropriately rejected based upon supposedly-prior work which was actually by the same authors and not previously published?
- What happens if the Program Chair has a conflict with the authors of a submitted paper?
- Some evidence about bias in merit reviewing been gathered below.
- What exactly do I have to do to anonymize my paper?
- I would like to provide supplementary material for consideration, e.g., the code of my implementation or proofs of theorems. How do I do this?
- Is there a way for me to submit anonymous supplementary material which could be considered by a reviewer before she submits her review (rather than potentially non-anonymous material that can only be viewed afterward)?
- Can I supplement my submission using a URL that links to auxiliary materials instead of submitting such materials to the HotCRP system directly?
- I am building on my own past work on the WizWoz system. Do I need to rename this system in my paper for purposes of anonymity, so as to remove the implied connection between my authorship of past work on this system and my present submission?
- I am submitting a paper that extends my own work that previously appeared at a workshop. Should I anonymize any reference to that prior work?
- Am I allowed to post my (non-blinded) paper on my web page? Can I advertise the unblinded version of my paper on mailing lists or send it to colleagues? May I give a talk about my work while it is under review?
- Will the fact that POPL is double-blind have an impact on handling conflicts-of interest? When I am asked by the submission system to identify conflicts of interest, what criteria should I use?
- What should I do if I if I learn the authors' identity? What should I do if a prospective POPL author contacts me and asks to visit my institution?
- The authors have provided a URL to supplementary material. I would like to see the material but I worry they will snoop my IP address and learn my identity. What should I do?
- If I am assigned a paper for which I feel I am not an expert, how do I seek an outside review?
- May I ask one of my students to do a review for me?
- What criteria do I use for identifying potential conflicts of interest?
- Are PC members allowed to submit papers? If so, how are they handled?
- How should I handle a paper I feel is very good, and yet would be a better fit for PLDI (or ICFP or OOPSLA)?
- How should I handle a paper that is out of scope for POPL?
General
Q: Why are you using double-blind reviewing?
A: Our goal is to give each a reviewer an unbiased "first look" at each paper. Studies have shown that a reviewer's attitude toward a submission may be affected, even unconsciously, by the identity of the author (see link below to more details). We want reviewers to be able to approach each submission without such involuntary reactions as "Barnaby; he writes a good paper" or "Who are these people? I have never heard of them." For this reason, we ask that authors to omit their names from their submissions, and that they avoid revealing their identity through citation. Note that many systems and security conferences use double-blind reviewing and have done so for years (e.g., SIGCOMM, OSDI, IEEE Security and Privacy, SIGMOD). POPL and PLDI have done it for the last several years.
A key principle to keep in mind is that we intend this process to be cooperative, not adversarial. If a reviewer does discover an author's identity though a subtle clue or oversight the author will not be penalized.
For those wanting more information, see the list of studies about gender bias in other fields and links to CS-related articles that cover this and other forms of bias below.
A: Studies of blinding with the flavor we are using show that author identities remain unknown 53% to 79% of the time (see Snodgrass, linked below, for details). Moreover, about 5-10% of the time (again, see Snodgrass), a reviewer is certain of the authors, but then turns out to be at least partially mistaken. So, while sometimes authorship can be guessed correctly, the question is, is imperfect blinding better than no blinding at all? If author names are not explicitly in front of the reviewer on the front page, does that help at all even for the remaining submissions where it would be possible to guess? Our conjecture is that on balance the answer is "yes".
A: I have heard of this happening, and this is indeed a serious issue. In the approach we are taking for POPL, author names are revealed to reviewers after they have submitted their review. Therefore, a reviewer can correct their review if they indeed have penalized the authors inappropriately. Unblinding prior to the PC meeting also avoids abuses in which committee members end up advancing the cause of a paper with which they have a conflict.
Q: What happens if the Program Chair has a conflict with the authors of a submitted paper?
A: Ranjit Jhala, POPL 2018 General Chair, has agreed to help manage the reviewing process for papers with which the Program Chair has a conflict.
For authors
Q: What exactly do I have to do to anonymize my paper?A: Your job is not to make your identity undiscoverable but simply to make it possible for our reviewers to evaluate your submission without having to know who you are. The specific guidelines stated in the call for papers are simple: omit authors' names from your title page (or list them as "omitted for submission"), and when you cite your own work, refer to it in the third person. For example, if your name is Smith and you have worked on amphibious type systems, instead of saying "We extend our earlier work on statically typed toads (Smith 2004)," you might say "We extend Smith's (2004) earlier work on statically typed toads." Also, be sure not to include any acknowledgements that would give away your identity. If you have any questions, feel free to ask the PC chair.
A: On the submission site there is an option to submit supplementary material along with your main paper. Two forms of supplementary material may be submitted.
- Anonymous supplementary material is available to the reviewers before they submit their first-draft reviews.
- Non-anonymous supplementary material is available to the reviewers only after they have submitted their first-draft reviews and learnt the identity of the authors.
The submission itself is the object of review and so it should strive to convince the reader of at least the plausibility of reported results; supplementary material only serves to confirm, in more detail, the idea argued in the paper. Of course, reviewers are free to change their review upon viewing supplementary material (or for any other reason). For those authors who wish to supplement, we encourage them to mention the supplement in the body of the paper so reviewers know to look for it, if necessary. E.g., “The proof of Lemma 1 is included in the non-anonymous supplementary material submitted with this paper.”
A: Yes, see previous answer. The option of anonymous supplementary material is new for POPL 2017. Previously, authors have been known to release a TR, code, etc. via an anonymous hosting service, and to include a URL to that material in the paper. We discourage authors from using such tactics except for materials that cannot, for some reason, be uploaded to the official site (e.g., a live demo). We emphasize that authors should strive to make their paper as convincing as possible within the submission page limit, in case reviewers choose not to access supplementary material. Also, see the next question.
A In general, we discourage authors from providing supplementary materials via links to external web sites. It is possible to change the linked items after the submission deadline has passed, and, to be fair to all authors, we would like to be sure reviewers evaluate materials that have been completed prior to the submission deadline. Having said that, it is appropriate to link to items, such as an online demo, that can't easily be submitted. Needless to say, attempting to discover the reviewers for your paper by tracking visitors to such a demo site would be a breach of academic integrity. Supplementary items such as PDFs should always be uploaded to HotCRP.
A: No. The relationship between systems and authors changes over time, so there will be at least some doubt about authorship. Increasing this doubt by changing the system name would help with anonymity, but it would compromise the research process. In particular, changing the name requires explaining a lot about the system again because you can't just refer to the existing papers, which use the proper name. Not citing these papers runs the risk of the reviewers who know about the existing system thinking you are replicating earlier work. It is also confusing for the reviewers to read about the paper under Name X and then have the name be changed to Name Y. Will all the reviewers go and re-read the final version with the correct name? If not, they have the wrong name in their heads, which could be harmful in the long run.
A: No. But we recommend you do not use the same title for your POPL submission, so that it is clearly distinguished from the prior paper. In general there is rarely a good reason to anonymize a citation. One possibility is for work that is tightly related to the present submission and is also under review. But such works may often be non-anonymous. When in doubt, contact the PC Chair.
A: As far as the authors' publicity actions are concerned, a paper under double-blind review is largely the same as a paper under regular (single-blind) review. Double-blind reviewing should not hinder the usual communication of results.
That said, we do ask that you not attempt to deliberately subvert the double-blind reviewing process by announcing the names of the authors of your paper to the potential reviewers of your paper. It is difficult to define exactly what counts as "subversion" here, but a blatant example might include sending individual e-mail to members of the PC about your work (unless they are conflicted out anyway). On the other hand, it is perfectly fine, for example, to visit other institutions and give talks about your work, to present your submitted work during job interviews, to present your work at professional meetings (e.g. Dagstuhl), or to post your work on your web page. In general, PC members will not be asked to recuse themselves if they discover the (likely) identity of an author through such means. If you're not sure about what constitutes "subversion", please consult directly with the Program Chair.
A: Using DBR does not change the principle that reviewers should not review papers with which they have a conflict of interest, even if they do not immediately know who the authors are. Quoting (with slight alteration) from the ACM SIGPLAN review policies document:
A conflict of interest is defined as a situation in which the reviewer can be viewed as being able to benefit personally in the process of reviewing a paper. For example, if a reviewer is considering a paper written by a member of his own group, a current student, his advisor, or a group that he is seen as being in close competition with, then the outcome of the review process can have direct benefit to the reviewer's own status. If a conflict of interest exists, the potential reviewer should decline to review the paper.As an author, you should list PC members (and any others, since others may be asked for outside reviewers) which you believe have a conflict with you. While particular criteria for making this determination may vary, please apply the following guidelines, identifying a potential reviewer Bob as conflicted if
- Bob was your co-author or collaborator at some point within the last 2 years
- Bob is an advisor or advisee of yours
- Bob is a family member
- Bob has a non-trivial financial stake in your work (e.g., invested in your startup company)
If a possible reviewer does not meet the above criteria, please do not identify him/her as conflicted. Doing so could be viewed as an attempt to prevent a qualified, but possibly skeptical reviewer from reviewing your paper. If you nevertheless believe that a reviewer who does not meet the above criteria is conflicted, you may identify the person and send a note to the PC Chair.
For reviewers
A: If at any point you feel that the authors' actions are largely aimed at ensuring that potential reviewers know their identity, you should contact the Program Chair. Otherwise you should not treat double-blind reviewing differently from regular blind reviewing. In particular, you should refrain from seeking out information on the authors' identity, but if you discover it accidentally this will not automatically disqualify you as a reviewer. Use your best judgment.
A: Contact the Program Chair, who will download the material on your behalf and make it available to you.
Q: If I am assigned a paper for which I feel I am not an expert, how do I seek an outside review?
A: PC members should do their own reviews, not delegate them to someone else. If doing so is problematic for some papers, e.g., you don't feel completely qualified, then consider the following options. First, submit a review for your paper that is as careful as possible, outlining areas where you think your knowledge is lacking. Assuming we have sufficient expert reviews, that could be the end of it: non-expert reviews are valuable too, since conference attendees are by-and-large not experts for any given paper. Second, if you feel like the gaps in your knowledge are substantial, submit a first-cut review, and then work with the PC chair to solicit an external review. This is easy: after submitting your review the paper is unblinded, so you at least know not to solicit the authors! You will also know other reviewers of the paper that have already been solicited. If none of these expert reviewers is acceptable to you, just check with the PC Chair that the person you do wish to solicit is not conflicted with the authors. In addition, the PC chair will attempt to balance the load on external reviewers. Keep in mind that while we would like the PC to make as informed a decision as possible about each submitted paper, each additional review we solicit places a burden on the community.
As a last resort, if you feel like your review would be extremely uninformed and you'd rather not even submit a first cut, contact the PC Chair, and another reviewer will be assigned.
Q: May I ask one of my students to do a review for me?
A: Having students (or interns at a research lab) participate in the review process is good for their education. However, you should not just "offload" your reviews to your students. Each review assigned to you is your responsibility. We recommend the following process: If you are sure that your student's conflicts of interest are a subset of your own, you and your student may both begin to do your own separate reviews in parallel. (A student's review should never simply be a substitute for your own work.) If your student's conflicts of interest are not a subset of your own, you may do your own first-cut review first and then unblind the authors so you can check, or you may consult with the PC chair. Either way, once the student has completed their review, you should check the review to ensure the tone is professional and the content is appropriate. Then you may merge the student's review with your own.
Q: How do we handle potential conflicts of interest since I cannot see the author names?
A: The conference review system will ask that you identify conflicts of interest when you get an account on the submission system. Please see the related question applied to authors to decide how to identify conflicts. Feel free to also identify additional authors whose papers you feel you could not review fairly for reasons other than those given (e.g., strong personal friendship).
Q: Are PC members allowed to submit papers? If so, how are they handled?
A: PC members are allowed to submit papers. However, since SIGPLAN mandates that PC member papers be held to a "higher standard," truly borderline PC papers will not receive the benefit of the doubt, whereas a regular non-PC paper might.
A: The scope of POPL is broad and encompasses all topics that pertain to programming language theory, design and implementation. Hence, if you feel a paper would be an excellent PLDI (or ICFP or OOPSLA) paper then it would also be an excellent POPL paper. To be accepted at POPL, a paper must discuss programming languages in some way, shape or form and it must have the potential to make a lasting impact on our field.
Q: How should I handle a paper that is out of scope for POPL?
A: The scope of POPL is broad and encompasses all topics that pertain to programming language theory, design and implementation. However, if you discover you have been assigned a paper that does not contribute to the study of programming languages, please contact the program chair. We will discuss it and may decide to reject the paper on grounds of scope. Of course, if we decide after all that the paper is within the scope of POPL, you should review it like any other paper.
More information about bias in merit reviewing
Note that this information was put together by the program chair; not all program or external review committee members are necessarily persuaded by it.
Kathryn McKinley's editorial makes the case for double-blind reviewing from a computer science perspective. Her article cites Richard Snodgrass's SIGMOD record editorial which collects many studies of the effects of potential bias in peer review.
Here are a few studies on the potential effects of bias manifesting in a merit review process, focusing on bias against women. (These were collected by David Wagner.)
- There's the famous story of gender bias in orchestra try-outs, where moving to blind auditions seems to have increased the hiring of female musicians by up to 33% or so. Today some orchestras even go so far as to ask musicians to remove their shoes (or roll out thick carpets) before auditioning, to try to prevent gender-revealing cues from the sound of the auditioner's shoes.
- One study found bias in assessment of identical CVs but with names and genders changed. In particular, the researchers mailed out c.v.'s for a faculty position, but randomly swapped the gender of the name on some of them. They found that both men and women reviewers ranked supposedly-male job applicants higher than supposedly-female applicants -- even though the contents of the c.v. were identical. Presumably, none of the reviewers thought of themselves as biased, yet their evaluations in fact exhibited gender bias. (However: in contrast to the gender bias at hiring time, if the reviewers were instead asked to evaluate whether a candidate should be granted tenure, the big gender differences disappeared. For whatever that's worth.)
- The Implicit Association Test illustrates how factors can bias our decision-making, without us realising it. For instance, a large fraction of the population has a tendency to associate men with career (professional life) and women with family (home life), without realizing it. The claim is that we have certain gender stereotypes and schemas which unconsciously influence the way we think. The interesting thing about the IAT is that you can take it yourself. If you want to give it a try, select the Gender-Career IAT or the Gender-Science IAT from here. There's evidence that these unconscious biases affect our behavior. For instance, one study of recommendation letters written for 300 applicants (looking only at the ones who were eventually hired) found that, when writing about men, letter-writers were more likely to highlight the applicant's research and technical skills, while when writing about women, letter-writers were more likely to mention the applicant's teaching and interpersonal skills.
- There's a study of postdoctoral funding applications in Sweden, which found that women needed to be about 2.5 times as productive (in terms of papers published) as men, to be ranked equivalently. Other studies have suggested that the Swedish experience may be an anomaly. (For instance, one meta-analysis I saw estimated that, on average, it appears men win about 7% more grant applications than women, but since this is not controlled according to the objective quality of the application, it does not necessarily imply the presence of gender bias in reviewing of grant applications.)
- This study reports experience from an ecology journal that switched from non-blind to blind reviewing. After the switch, they found a significant (~8%) increase in the acceptance rate for female-first-authored submissions. To put it another way, they saw a 33% increase in the fraction of published papers whose first author is female (28% -> 37%). Keep in mind that this is not a controlled experiment, so it proves correlation but not causation, and there appears to be controversy in the literature about the work. So it as at most a plausibility result that gender bias could be present in the sciences, but far from definitive.
Snodgrass' studies includes some of these, and more.