This page will soon grow in content and contain information about the scope of this research track.
Wed 20 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10 | Track 1: Algorithmic VerificationResearch Papers at Grand Bay North Chair(s): Arie GurfinkelCarnegie Mellon University | ||
10:30 25mTalk | Temporal Verification of Higher-order Functional Programs Research Papers Akihiro Murase, Tachio TerauchiJAIST, Naoki KobayashiUniversity of Tokyo, Ryosuke SatoUniversity of Tokyo, Hiroshi UnnoUniversity of Tsukuba | ||
10:55 25mTalk | Scaling Network Verification using Symmetry and Surgery Research Papers Gordon Plotkin, Nikolaj BjørnerMicrosoft Research, Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research, George VargheseMicrosoft Research | ||
11:20 25mTalk | Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates Research Papers | ||
11:45 25mTalk | Reducing Crash Recoverability to Reachability Research Papers |
10:30 - 12:10 | Track 2: Types and FoundationsResearch Papers at Grand Bay South Chair(s): Robert AtkeyUniversity of Strathclyde | ||
10:30 25mTalk | Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega Research Papers Media Attached File Attached | ||
10:55 25mTalk | Type Theory in Type Theory using Quotient Inductive Types Research Papers Media Attached File Attached | ||
11:20 25mTalk | System Fω with Equirecursive Types for Datatype-generic Programming Research Papers Yufei CaiUniversity of Tübingen, Germany, Paolo G. GiarrussoUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany Media Attached | ||
11:45 25mTalk | A Theory of Effects and Resources: Adjunction Models and Polarised Calculi Research Papers Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo FioreComputer Laboratory, University of Cambridge, Guillaume Munch-MaccagnoniComputer Laboratory, University of Cambridge |
14:20 - 16:00 | Track 1: Decision ProceduresResearch Papers at Grand Bay North Chair(s): Loris D'AntoniUniversity of Pennsylvania | ||
14:20 25mTalk | Query-Guided Maximum Satisfiability Research Papers Xin ZhangGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Aditya NoriMicrosoft Research, UK, Mayur NaikGeorgia Tech File Attached | ||
14:45 25mTalk | String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS Research Papers Media Attached | ||
15:10 25mTalk | Symbolic Computation of Differential Equivalences Research Papers Luca CardelliMicrosoft Research and University of Oxford, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinIMT Institute for Advanced Studies Lucca, Italy Media Attached | ||
15:35 25mTalk | Unboundedness and Downward Closures of Higher-Order Pushdown Automata Research Papers Matthew HagueRoyal Holloway University of London, UK, Jonathan KochemsDepartment of Computer Science, University of Oxford, C.-H. Luke OngUniversity of Oxford, UK Media Attached |
14:20 - 16:00 | Track 2: Correct CompilationResearch Papers at Grand Bay South Chair(s): Jens PalsbergUniversity of California, Los Angeles | ||
14:20 25mTalk | Fully-Abstract Compilation by Approximate Back-Translation Research Papers Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven Pre-print Media Attached | ||
14:45 25mTalk | Lightweight Verification of Separate Compilation Research Papers Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany Media Attached File Attached | ||
15:10 25mTalk | From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes Research Papers Media Attached | ||
15:35 25mTalk | Sound Type-dependent Syntactic Language Extension Research Papers Pre-print Media Attached File Attached |
16:30 - 17:45 | Track 2: Decidability and complexityResearch Papers at Grand Bay South Chair(s): C.-H. Luke OngUniversity of Oxford, UK | ||
16:30 25mTalk | Decidability of Inferring Inductive Invariants Research Papers Oded PadonTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Sharon Shoham, Aleksandr KarbyshevTel Aviv University, Mooly SagivTel Aviv University Media Attached | ||
16:55 25mTalk | The Hardness of Data Packing Research Papers Media Attached | ||
17:20 25mTalk | The Complexity of Interaction Research Papers Media Attached |
19:00 - 22:00 | |||
Thu 21 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10 | Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North Chair(s): Mooly SagivTel Aviv University | ||
10:30 25mTalk | Certified Causally Consistent Distributed Key-Value Stores Research Papers Media Attached | ||
10:55 25mTalk | 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems Research Papers Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6 Media Attached | ||
11:20 25mTalk | A Program Logic for Concurrent Objects under Fair Scheduling Research Papers Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China Media Attached | ||
11:45 25mTalk | PSync: a partially synchronous language for fault-tolerant distributed algorithms Research Papers Link to publication DOI Pre-print Media Attached File Attached |
10:30 - 12:10 | Track 2: Probabilistic and statistical analysisResearch Papers at Grand Bay South Chair(s): Aditya NoriMicrosoft Research, UK | ||
10:30 25mTalk | Prophet: Automatic Patch Generation via Learning from Successful Patches Research Papers Media Attached | ||
10:55 25mTalk | Estimating types in binaries using predictive modeling Research Papers Omer KatzTechnion, Israel Institute of Technology, Ran El-YanivTechnion, Israel Institute of Technology, Eran YahavTechnion Media Attached File Attached | ||
11:20 25mTalk | Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs Research Papers Krishnendu ChatterjeeIST Austria, Hongfei FuIST Austria, Rouzbeh HasheminezhadSharif University, Petr NovotnyIST Austria Media Attached | ||
11:45 25mTalk | Transforming Spreadsheet Data Types using Examples Research Papers Media Attached |
14:20 - 16:00 | Track 1: Learning and verificationResearch Papers at Grand Bay North Chair(s): David MonniauxCNRS, VERIMAG | ||
14:20 25mTalk | Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis Research Papers Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg Media Attached | ||
14:45 25mTalk | Abstraction Refinement Guided by a Learnt Probabilistic Model Research Papers Media Attached | ||
15:10 25mTalk | Learning Invariants using Decision Trees and Implication Counterexamples Research Papers Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity of Illinois at Urbana-Champaign Media Attached | ||
15:35 25mTalk | Symbolic Abstract Data Type Inference Research Papers Media Attached |
14:20 - 16:00 | Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South Chair(s): Tiark RompfPurdue & Oracle Labs | ||
14:20 25mTalk | Principal Type Inference for GADTs Research Papers Media Attached | ||
14:45 25mTalk | Abstracting Gradual Typing Research Papers Link to publication Media Attached | ||
15:10 25mTalk | The Gradualizer: a methodology and algorithm for generating gradual type systems Research Papers Media Attached | ||
15:35 25mTalk | Is Sound Gradual Typing Dead? Research Papers Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern University Pre-print Media Attached File Attached |
16:30 - 17:45 | |||
16:30 25mTalk | SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization Research Papers Somashekaracharya G BhaskaracharyaIndian Institute of Science and National Instruments, Uday BondhugulaIndian Institute of Science, Albert CohenINRIA Media Attached File Attached | ||
16:55 25mTalk | PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs Research Papers Wenlei Bao, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noël PouchetOhio State University, Fabrice RastelloINRIA, France, P. SadayappanOhio State University Media Attached | ||
17:20 25mTalk | Printing Floating-Point Numbers: A Faster, Always Correct Method Research Papers Marc AndryscoUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego Media Attached |
16:30 - 17:45 | Track 2: Sessions and processesResearch Papers at Grand Bay South Chair(s): Matteo MaffeiSaarland University | ||
16:30 25mTalk | Effects as sessions, sessions as effects Research Papers Pre-print Media Attached | ||
16:55 25mTalk | Monitors and Blame Assignment for Higher-Order Session Types Research Papers Limin JiaCarnegie Mellon University, Hannah GommerstadtCarnegie Mellon University, Frank PfenningCarnegie Mellon University Media Attached File Attached | ||
17:20 25mTalk | Environmental Bisimulations for Probabilistic Higher-Order Languages Research Papers Media Attached |
18:00 - 19:00 | SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business MeetingResearch Papers at Grand Bay North Chair(s): Michael HicksUniversity of Maryland at College Park, USA | ||
Fri 22 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10 | Track 1: Program Design and AnalysisResearch Papers at Grand Bay North Chair(s): Manu SridharanSamsung Research America | ||
10:30 25mTalk | Newtonian Program Analysis via Tensor Product Research Papers Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogle Media Attached | ||
10:55 25mTalk | Casper: An Efficient Approach to Call Trace Collection Research Papers Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao XiaoThe Hong Kong University of Science and Technology, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu ZhangMicrosoft Research, Charles ZhangHKUST Media Attached | ||
11:20 25mTalk | Pushdown Control-flow Analysis for Free Research Papers Thomas GilrayUniversity of Utah, Steven Lyde, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland, College Park Pre-print Media Attached | ||
11:45 25mTalk | Binding as Sets of Scopes Research Papers Matthew FlattUniversity of Utah Pre-print Media Attached |
10:30 - 12:10 | Track 2: Semantics and memory modelsResearch Papers at Grand Bay South Chair(s): Alexey GotsmanIMDEA | ||
10:30 25mTalk | Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA Research Papers Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity of Cambridge Media Attached File Attached | ||
10:55 25mTalk | A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions Research Papers File Attached | ||
11:20 25mTalk | Overhauling SC atomics in C11 and OpenCL Research Papers John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London Pre-print File Attached | ||
11:45 25mTalk | Taming Release-Acquire Consistency Research Papers Pre-print Media Attached File Attached |
14:20 - 15:35 | Track 2: Foundations of Model CheckingResearch Papers at Grand Bay South Chair(s): Alexandra SilvaRadboud University Nijmegen | ||
14:20 25mTalk | Lattice-Theoretic Progress Measures and Coalgebraic Model Checking Research Papers Ichiro HasuoUniversity of Tokyo, Shunsuke ShimizuUniversity of Tokyo, Corina CirsteaUniversity of Southampton Media Attached | ||
14:45 25mTalk | Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components Research Papers Krishnendu ChatterjeeIST Austria, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis Media Attached | ||
15:10 25mTalk | Memoryful Geometry of Interaction II: Recursion and Adequacy Research Papers Media Attached |
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.
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.
Important Dates
Paper registration | 3 July 2015, AOE |
Paper submission | 10 July 2015, AOE |
Submission URL | https://popl16.hotcrp.com/ |
Author response period | 17 September, 12:00 noon CET - 20 September, 11:00pm CET |
Author notification | 05 October 2015 |
Camera-ready deadline | 05 November 2015 |
Main conference | 20-22 January 2016 |
Co-located events | 17-19, 23 January 2016 |
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 at least 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 are submitted late will be rejected. All deadlines are firm.
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. It will be made available to reviewers only after they have submitted their first-draft reviews and hence need not be anonymized. 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.
Templates for ACM format are available for Word Perfect, 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.
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.)
POPL 2016 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 ...").
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. Additional information is to be found on the POPL AEC web page. 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.
Accepted Papers
Proceedings
POPL 2016- Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
