POPL 2017 - POPL 2017 (original) (raw)
This is the main track of POPL 2017, featuring research papers and invited talks. Please select a tab for more information.
News
The POPL 2017 program is available.
The full POPL 2017 proceedings are accessible.
The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.
Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone
The GMT offsets shown reflect the offsets at the moment of the conference.
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full programSpecify a time band
-
You're viewing the program in a time zone which is different from your device's time zone change time zone
| 10:30 - 12:10 | Abstract InterpretationPOPL at Amphitheater 44 Chair(s): Isabella Mastroeni University of Verona, Italy |
|---|---|
| 10:3025mTalk | **Ogre and Pythia, An invariance proof method for weak consistency models**POPLJade Alglave University College London, Patrick Cousot New York University |
| 10:5525mTalk | **A Posteriori Environment Analysis with Pushdown Delta CFA**POPLKimball Germane University of Utah, Matthew Might University of Utah; Harvard Medical School; The White House |
| 11:2025mTalk | **Semantic-Directed Clumping of Disjunctive Abstract States**POPLHuisong Li INRIA/CNRS/ENS/PSL*, François Bérenger INRIA/CNRS/ENS/PSL*, Bor-Yuh Evan Chang University of Colorado Boulder, Xavier Rival INRIA/CNRS/ENS Paris |
| 11:4525mTalk | **Fast Polyhedra Abstract Domain**POPLGagandeep Singh ETH Zurich, Switzerland, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich |
| 10:30 - 12:10 | Type Systems 1POPL at Auditorium Chair(s): Avik Chaudhuri Facebook |
|---|---|
| 10:3025mTalk | **Polymorphism, subtyping and type inference in MLsub**POPLStephen Dolan , Alan Mycroft University of Cambridge |
| 10:5525mTalk | **Java generics are Turing complete**POPLRadu Grigore University of Kent |
| 11:2025mTalk | **Hazelnut: A Bidirectionally Typed Structure Editor Calculus**POPLCyrus Omar Carnegie Mellon University, Ian Voysey Carnegie Mellon University, Michael Hilton Oregon State University, USA, Jonathan Aldrich Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder |
| 11:4525mTalk | **Modules, Abstraction, and Parametric Polymorphism**POPLKarl Crary Carnegie Mellon University |
| 14:20 - 16:00 | Probabilistic ProgrammingPOPL at Amphitheater 44 Chair(s): Marco Gaboardi SUNY Buffalo, USA |
|---|---|
| 14:2025mTalk | **Beginner's Luck: A Language for Property-Based Generators**POPLLeonidas Lampropoulos University of Pennsylvania, Diane Gallois-Wong Inria Paris, ENS Paris, Cătălin Hriţcu Inria Paris, John Hughes Chalmers University of Technology, Benjamin C. Pierce University of Pennsylvania, Li-yao Xia ENS Paris Pre-print |
| 14:4525mTalk | **Exact Bayesian Inference by Symbolic Disintegration**POPLChung-chieh Shan Indiana University, USA, Norman Ramsey Pre-print |
| 15:1025mTalk | **Stochastic Invariants for Probabilistic Termination**POPLKrishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge |
| 15:3525mTalk | **Coupling proofs are probabilistic product programs**POPLGilles Barthe IMDEA, Benjamin Gregoire INRIA, Justin Hsu , Pierre-Yves Strub École Polytechnique |
| 16:30 - 17:45 | Compiler OptimisationPOPL at Auditorium Chair(s): Andrew Myers Cornell University |
|---|---|
| 16:3025mTalk | **A Program Optimization for Automatic Database Result Caching**POPLZiv Scully Carnegie Mellon University, Adam Chlipala MIT |
| 16:5525mTalk | **Stream Fusion, to Completeness**POPLOleg Kiselyov , Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens Pre-print Media Attached |
| 17:2025mTalk | **Rigorous Floating-point Mixed Precision Tuning**POPLWei-Fan Chiang School of Computing, University of Utah, Ganesh Gopalakrishnan University of Utah, Zvonimir Rakamaric University of Utah, Ian Briggs School of Computing, University of Utah, Marek S. Baranowski University of Utah, Alexey Solovyev School of Computing, University of Utah Pre-print |
| 10:30 - 12:10 | Program AnalysisPOPL at Amphitheater 44 Chair(s): Francesco Logozzo Facebook |
|---|---|
| 10:3025mTalk | **Relational Cost Analysis**POPLEzgi Çiçek MPI-SWS, Germany, Gilles Barthe IMDEA, Marco Gaboardi SUNY Buffalo, USA, Deepak Garg MPI-SWS, Germany, Jan Hoffmann Carnegie Mellon University |
| 10:5525mTalk | **Contract-based Resource Verification for Higher-order Functions with Memoization**POPLRavichandhran Madhavan EPFL, Sumith Kulal IIT Bombay, Viktor Kunčak EPFL, Switzerland |
| 11:2025mTalk | **Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability**POPLQirun Zhang University of California, Davis, Zhendong Su University of California, Davis |
| 11:4525mTalk | **Towards Automatic Resource Bound Analysis for OCaml**POPLJan Hoffmann Carnegie Mellon University, Ankush Das Carnegie Mellon University, Shu-chun Weng Yale University |
| 14:20 - 16:00 | Concurrency 2POPL at Amphitheater 44 Chair(s): Nobuko Yoshida Imperial College London, UK |
|---|---|
| 14:2025mTalk | **Mixed-size Concurrency: ARM, POWER, C/C++11, and SC**POPLShaked Flur University of Cambridge, Susmit Sarkar University of St. Andrews, UK, Christopher Pulte University of Cambridge, Kyndylan Nienhuis University of Cambridge, Luc Maranget INRIA Rocquencourt, Kathryn E. Gray University of Cambridge, Ali Sezgin University of Cambridge, Mark Batty University of Kent, Peter Sewell University of Cambridge |
| 14:4525mTalk | **Dynamic Race Detection For C++11**POPLChristopher Lidbury Imperial College London, Alastair F. Donaldson Imperial College London |
| 15:1025mTalk | **Serializability for Eventual Consistency: Criterion, Analysis and Applications**POPLLucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zurich Pre-print |
| 15:3525mTalk | **Thread Modularity at Many Levels: a Pearl in Compositional Verification**POPLJochen Hoenicke Universität Freiburg, Rupak Majumdar MPI-SWS, Andreas Podelski University of Freiburg, Germany |
| 14:20 - 16:00 | Functional Programming with EffectsPOPL at Auditorium Chair(s): Kathleen Fisher Tufts University |
|---|---|
| 14:2025mTalk | **Type Directed Compilation of Row-Typed Algebraic Effects**POPLDaan Leijen Microsoft Research |
| 14:4525mTalk | **Do be do be do**POPLSam Lindley University of Edinburgh, Conor McBride , Craig McLaughlin The University of Edinburgh |
| 15:1025mTalk | **Dijkstra Monads for Free**POPLDanel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin , Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research Pre-print |
| 15:3525mTalk | **Stateful Manifest Contracts**POPLTaro Sekiyama , Atsushi Igarashi Kyoto University |
| 16:30 - 17:20 | Semantic FoundationsPOPL at Amphitheater 44 Chair(s): Lars Birkedal Aarhus University |
|---|---|
| 16:3025mTalk | **A Semantic Account of Metric Preservation**POPLArthur Azevedo de Amorim University of Pennsylvania, USA, Ikram Cherigui ENS Paris, Marco Gaboardi SUNY Buffalo, USA, Justin Hsu , Shin-ya Katsumata Kyoto University |
| 16:5525mTalk | **Cantor Meets Scott: Semantic Foundations for Probabilistic Networks**POPLSteffen Smolka Cornell University, Praveen Kumar Cornell University, Nate Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London DOI File Attached |
| 10:30 - 12:10 | Verification and SynthesisPOPL at Amphitheater 44 Chair(s): Benjamin Delaware Purdue University |
|---|---|
| 10:3025mTalk | **Component-Based Synthesis for Complex APIs**POPLYu Feng University of Texas at Austin, USA, Ruben Martins , Yuepeng Wang University of Texas at Austin, Işıl Dillig UT Austin, Thomas Reps University of Wisconsin - Madison and Grammatech Inc. |
| 10:5525mTalk | **Learning nominal automata**POPLJoshua Moerman Radboud University, Matteo Sammartino University College London, Alexandra Silva University College London, Bartek Klin University of Warsaw, Michał Szynwelski University of Warsaw |
| 11:2025mTalk | **On Verifying Causal Consistency**POPLAhmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea LIAFA, Université Paris Diderot, Rachid Guerraoui , Jad Hamza LIAFA, Université Paris Diderot |
| 11:4525mTalk | **Complexity Verification Using Guided Theorem Enumeration**POPLAkhilesh Srikanth Georgia Institute of Technology, Burak Sahin Georgia Institute of Technology, William Harris |
| 14:20 - 16:00 | Concurrency 3POPL at Amphitheater 44 Chair(s): Adam Chlipala MIT |
|---|---|
| 14:2025mTalk | **Parallel Functional Arrays**POPLAnanya Kumar , Guy E. Blelloch Carnegie Mellon University, Robert Harper |
| 14:4525mTalk | **A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms**POPLIgor Konnov TU Wien, Marijana Lazić TU Wien, Helmut Veith TU Wien, Josef Widder TU Wien DOI Pre-print |
| 15:1025mTalk | **Analyzing divergence in bisimulation semantics**POPLXinxin Liu Institute of software, Chinese academy of sciences, Tingting Yu , Wenhui Zhang Institute of software, Chinese academy of sciences |
| 15:3525mTalk | **Fencing off Go: Liveness and Safety for Channel-Based Programming**POPLJulien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UK Pre-print |
| 16:30 - 17:45 | QuantumPOPL at Amphitheater 44 Chair(s): Michele Pagani IRIF, Université Paris Diderot |
|---|---|
| 16:3025mTalk | **Invariants of Quantum Programs: Characterisations and Generation**POPLMingsheng Ying University of Technology Sydney, Australia, Shenggang Ying University of Technology Sydney, Australia, Xiaodi Wu University of Oregon, USA |
| 16:5525mTalk | **The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects**POPLUgo Dal Lago University of Bologna, France, Claudia Faggian , Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay, Akira Yoshimizu Univ.Tokyo |
| 17:2025mTalk | **QWIRE: A Core Language for Quantum Circuits**POPLJennifer Paykin , Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania |
Accepted 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. Papers discussing new ideas and new areas are encouraged, as are papers (often called “pearls”) that elucidate existing concepts in ways that yield new insights. We are looking for any submission with the potential to make enduring contributions to the theory, design, implementation or application of programming languages.
The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.
Evaluation
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.
Explaining a known idea in a new way may make as strong a contribution as inventing a new idea. Hence, we encourage the submission of pearls: elegant essays that explain an old idea, but do so in a new way that clarifies the idea and yields new insights. There is no formal separation of categories; pearls will be held to the same standards as any other paper.
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.
A document that details principles underlying organizational and reviewing policies can be found here.
A document containing frequently asked questions about the reviewing and submission process, especially as it pertains to double-blind reviewing, can be found here.
The Program Committee, displayed to the right, meets face-to-face to make the final selection; the Program Committee is assisted by a larger External Review Committee, also displayed to the right. PC papers are reviewed and selected entirely by the ERC.
Submission guidelines
Prior to the registration deadline, the authors will register their paper by uploading information on the submission title, abstract (of at most 300 words), authors, topics, and conflicts to the conference web site. Papers that are not registered on time will be rejected.
Prior to the final paper submission deadline, the authors will upload their full paper in double blind format and formatted according to the ACM proceedings format. Each paper should have no more than 12 pages of text, excluding bibliography, in 9 pt format. Papers may be resubmitted multiple times up until the deadline. The last version submitted before the deadline will be the version that is reviewed. Papers that exceed the length requirement or deviate from the expected format or are submitted late will be rejected.
Deadlines expire at midnight anywhere on earth on the Important Dates displayed to the right.
Templates for ACM format are available for Microsoft Word and LaTeX at http://www.sigplan.org/Resources/Author (use the 9 pt preprint template). Submissions should be in PDF and printable on US Letter and A4 sized paper.
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 2017 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 judgement 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 (e.g., 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 should 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 learnt 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.
Publication
Final versions of accepted papers are allowed up to 12 pages excluding the bibliography. In addition, at most two additional pages may be purchased at $200 per page. This additional amount will be due at registration for the conference.
AUTHORS TAKE NOTE: 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 your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.)