Write a Blog >>

This page will soon grow in content and contain information about the scope of this research track.

Dates
You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 1: Algorithmic VerificationResearch Papers at Grand Bay North
Chair(s): Arie Gurfinkel Carnegie Mellon University
10:30
25m
Talk
Temporal Verification of Higher-order Functional Programs
Research Papers
Akihiro Murase , Tachio Terauchi JAIST, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo, Hiroshi Unno University of Tsukuba
10:55
25m
Talk
Scaling Network Verification using Symmetry and Surgery
Research Papers
Gordon Plotkin , Nikolaj Bjørner Microsoft Research, Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research, George Varghese Microsoft Research
Pre-print
11:20
25m
Talk
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Research Papers
11:45
25m
Talk
Reducing Crash Recoverability to Reachability
Research Papers
Eric Koskinen Yale University, Junfeng Yang Columbia University
10:30 - 12:10
Track 2: Types and FoundationsResearch Papers at Grand Bay South
Chair(s): Robert Atkey University of Strathclyde
10:30
25m
Talk
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
Research Papers
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles
Media Attached File Attached
10:55
25m
Talk
Type Theory in Type Theory using Quotient Inductive Types
Research Papers
Thorsten Altenkirch University of Nottingham, Ambrus Kaposi University of Nottingham
Media Attached File Attached
11:20
25m
Talk
System Fω with Equirecursive Types for Datatype-generic Programming
Research Papers
Yufei Cai University of Tübingen, Germany, Paolo G. Giarrusso University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
Media Attached
11:45
25m
Talk
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Research Papers
Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo Fiore Computer Laboratory, University of Cambridge, Guillaume Munch-Maccagnoni Computer Laboratory, University of Cambridge
14:20 - 16:00
Track 1: Decision ProceduresResearch Papers at Grand Bay North
Chair(s): Loris D'Antoni University of Pennsylvania
14:20
25m
Talk
Query-Guided Maximum Satisfiability
Research Papers
Xin Zhang Georgia Tech, Ravi Mangal Georgia Institute of Technology, Aditya Nori Microsoft Research, UK, Mayur Naik Georgia Tech
File Attached
14:45
25m
Talk
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
Research Papers
Anthony Widjaja Lin Yale-NUS College, Singapore, Pablo Barcelo University of Chile, Chile
Media Attached
15:10
25m
Talk
Symbolic Computation of Differential Equivalences
Research Papers
Luca Cardelli Microsoft Research and University of Oxford, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin IMT Institute for Advanced Studies Lucca, Italy
Media Attached
15:35
25m
Talk
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
Research Papers
Matthew Hague Royal Holloway University of London, UK, Jonathan Kochems Department of Computer Science, University of Oxford, C.-H. Luke Ong University of Oxford, UK
Media Attached
14:20 - 16:00
Track 2: Correct CompilationResearch Papers at Grand Bay South
Chair(s): Jens Palsberg University of California, Los Angeles
14:20
25m
Talk
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Dominique Devriese iMinds - Distrinet, KU Leuven, Marco Patrignani KU Leuven, Frank Piessens iMinds - Distrinet, KU Leuven
Pre-print Media Attached
14:45
25m
Talk
Lightweight Verification of Separate Compilation
Research Papers
Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Chung-Kil Hur Seoul National University, Derek Dreyer MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Media Attached File Attached
15:10
25m
Talk
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Ed Robbins Kent, Andy King Kent, Tom Schrijvers KU Leuven
Media Attached
15:35
25m
Talk
Sound Type-dependent Syntactic Language Extension
Research Papers
Florian Lorenzen TU Berlin, Sebastian Erdweg TU Darmstadt, Germany
Pre-print Media Attached File Attached
16:30 - 17:45
Track 1: Language DesignResearch Papers at Grand Bay North
Chair(s): David Walker Princeton University
16:30
25m
Talk
Dependent Types and Multi-Monadic Effects in F*
Research Papers
Nikhil Swamy Microsoft Research, Cătălin Hriţcu INRIA Paris, Chantal Keller MSR-INRIA, Aseem Rastogi University of Maryland, College Park, Antoine Delignat-Lavaud INRIA, Simon Forest ENS, Karthikeyan Bhargavan INRIA, Cédric Fournet Microsoft Research, Pierre-Yves Strub IMDEA Software Institute, Markulf Kohlweiss Microsoft Research, Jean-Karim Zinzindohoué INRIA, Santiago Zanella-Béguelin Microsoft Research
Pre-print Media Attached
16:55
25m
Talk
Fabular: Regression Formulas as Probabilistic Programming
Research Papers
Johannes Borgström Uppsala University, Andrew D. Gordon Microsoft Research and University of Edinburgh, Long Ouyang Stanford University, Claudio Russo Microsoft Research, Adam Ścibior University of Cambridge, Marcin Szymczak University of Edinburgh
Media Attached
17:20
25m
Talk
Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Research Papers
Bjørn Bugge Grathwohl DIKU, University of Copenhagen, Fritz Henglein DIKU, Denmark, Ulrik Terp Rasmussen DIKU, University of Copenhagen, Kristoffer Aalund Søholm Jobindex, Denmark, Sebastian Paaske Tørholm Jobindex, Denmark
Media Attached
16:30 - 17:45
Track 2: Decidability and complexityResearch Papers at Grand Bay South
Chair(s): C.-H. Luke Ong University of Oxford, UK
16:30
25m
Talk
Decidability of Inferring Inductive Invariants
Research Papers
Oded Padon Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Sharon Shoham , Aleksandr Karbyshev Tel Aviv University, Mooly Sagiv Tel Aviv University
Media Attached
16:55
25m
Talk
The Hardness of Data Packing
Research Papers
Rahman Lavaee , Chen Ding University of Rochester
Media Attached
17:20
25m
Talk
The Complexity of Interaction
Research Papers
Stéphane Gimenez University of Innsbruck, Georg Moser University of Innsbruck
Media Attached
19:00 - 22:00

Thu 21 Jan

Displayed 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 Sagiv Tel Aviv University
10:30
25m
Talk
Certified Causally Consistent Distributed Key-Value Stores
Research Papers
Media Attached
10:55
25m
Talk
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Research Papers
Alexey Gotsman IMDEA, Hongseok Yang University of Oxford, UK, Carla Ferreira Universidade Nova Lisboa, Mahsa Najafzadeh UPMC & INRIA, Marc Shapiro Inria & LIP6
Media Attached
11:20
25m
Talk
A Program Logic for Concurrent Objects under Fair Scheduling
Research Papers
Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China
Media Attached
11:45
25m
Talk
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Research Papers
Cezara Drăgoi INRIA, ENS, CNRS, Thomas A. Henzinger IST Austria, Damien Zufferey MIT
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 Nori Microsoft Research, UK
10:30
25m
Talk
Prophet: Automatic Patch Generation via Learning from Successful Patches
Research Papers
Fan Long MIT CSAIL, Martin C. Rinard Massachusetts Institute of Technology, USA
Media Attached
10:55
25m
Talk
Estimating types in binaries using predictive modeling
Research Papers
Omer Katz Technion, Israel Institute of Technology, Ran El-Yaniv Technion, Israel Institute of Technology, Eran Yahav Technion
Media Attached File Attached
11:20
25m
Talk
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
Research Papers
Krishnendu Chatterjee IST Austria, Hongfei Fu IST Austria, Rouzbeh Hasheminezhad Sharif University, Petr Novotný IST Austria
Media Attached
11:45
25m
Talk
Transforming Spreadsheet Data Types using Examples
Research Papers
Rishabh Singh Microsoft Research, Sumit Gulwani Microsoft Research
Media Attached
14:20 - 16:00
Track 1: Learning and verificationResearch Papers at Grand Bay North
Chair(s): David Monniaux CNRS, VERIMAG
14:20
25m
Talk
Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
Research Papers
Damien Octeau University of Wisconsin and Pennsylvania State University, Somesh Jha University of Wisconsin, Madison, Matthew Dering Pennsylvania State University, Patrick McDaniel Pennsylvania State University, Alexandre Bartel Technical University Darmstadt, Hongyu Li Rice University, Jacques Klein University of Luxembourg, Yves Le Traon University of Luxembourg
Media Attached
14:45
25m
Talk
Abstraction Refinement Guided by a Learnt Probabilistic Model
Research Papers
Radu Grigore University of Oxford, Hongseok Yang University of Oxford, UK
Media Attached
15:10
25m
Talk
Learning Invariants using Decision Trees and Implication Counterexamples
Research Papers
Pranav Garg University of Illinois at Urbana-Champaign, Daniel Neider University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Dan Roth University of Illinois at Urbana-Champaign
Media Attached
15:35
25m
Talk
Symbolic Abstract Data Type Inference
Research Papers
Michael Emmi IMDEA Software Institute, Constantin Enea LIAFA, Université Paris Diderot
Media Attached
14:20 - 16:00
Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South
Chair(s): Tiark Rompf Purdue & Oracle Labs
14:20
25m
Talk
Principal Type Inference for GADTs
Research Papers
Sheng Chen University of louisiana at Lafayette, Martin Erwig Oregon State University
Media Attached
14:45
25m
Talk
Abstracting Gradual Typing
Research Papers
Ronald Garcia University of British Columbia, Alison M. Clark , Éric Tanter University of Chile, Chile
Link to publication Media Attached
15:10
25m
Talk
The Gradualizer: a methodology and algorithm for generating gradual type systems
Research Papers
Matteo Cimini Indiana University, Jeremy G. Siek Indiana University
Media Attached
15:35
25m
Talk
Is Sound Gradual Typing Dead?
Research Papers
Asumu Takikawa Northeastern University, Daniel Feltey Northeastern University, Ben Greenman Northeastern University, Max S. New , Jan Vitek Northeastern University, Matthias Felleisen Northeastern University
Pre-print Media Attached File Attached
16:30 - 17:45
Track 1: OptimizationResearch Papers at Grand Bay North
Chair(s): Mayur Naik Georgia Tech
16:30
25m
Talk
SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization
Research Papers
Somashekaracharya G Bhaskaracharya Indian Institute of Science and National Instruments, Uday Bondhugula Indian Institute of Science, Albert Cohen INRIA
Media Attached File Attached
16:55
25m
Talk
PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs
Research Papers
Wenlei Bao , Sriram Krishnamoorthy Pacific Northwest National Laboratories, Louis-Noël Pouchet Ohio State University, Fabrice Rastello INRIA, France, P. Sadayappan Ohio State University
Media Attached
17:20
25m
Talk
Printing Floating-Point Numbers: A Faster, Always Correct Method
Research Papers
Marc Andrysco University of California, San Diego, Ranjit Jhala University of California, San Diego, Sorin Lerner University of California, San Diego
Media Attached
16:30 - 17:45
Track 2: Sessions and processesResearch Papers at Grand Bay South
Chair(s): Matteo Maffei Saarland University
16:30
25m
Talk
Effects as sessions, sessions as effects
Research Papers
Dominic Orchard Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print Media Attached
16:55
25m
Talk
Monitors and Blame Assignment for Higher-Order Session Types
Research Papers
Limin Jia Carnegie Mellon University, Hannah Gommerstadt Carnegie Mellon University, Frank Pfenning Carnegie Mellon University
Media Attached File Attached
17:20
25m
Talk
Environmental Bisimulations for Probabilistic Higher-Order Languages
Research Papers
Davide Sangiorgi University of Bologna, Valeria Vignudelli University of Bologna/INRIA
Media Attached
18:00 - 19:00
SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business MeetingResearch Papers at Grand Bay North
Chair(s): Michael Hicks University of Maryland at College Park, USA

Fri 22 Jan

Displayed 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 Sridharan Samsung Research America
10:30
25m
Talk
Newtonian Program Analysis via Tensor Product
Research Papers
Thomas Reps University of Wisconsin - Madison and Grammatech Inc., Emma Turetsky CS Dept., Univ. of Wisconsin-Madison, Prathmesh Prabhu Google
Media Attached
10:55
25m
Talk
Casper: An Efficient Approach to Call Trace Collection
Research Papers
Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao Xiao The Hong Kong University of Science and Technology, Shing-Chi Cheung Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu Zhang Microsoft Research, Charles Zhang HKUST
Media Attached
11:20
25m
Talk
Pushdown Control-flow Analysis for Free
Research Papers
Thomas Gilray University of Utah, Steven Lyde , Michael D. Adams University of Utah, Matthew Might University of Utah, USA, David Van Horn University of Maryland, College Park
Pre-print Media Attached
11:45
25m
Talk
Binding as Sets of Scopes
Research Papers
Matthew Flatt University of Utah
Pre-print Media Attached
10:30 - 12:10
Track 2: Semantics and memory modelsResearch Papers at Grand Bay South
Chair(s): Alexey Gotsman IMDEA
10:30
25m
Talk
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Research Papers
Shaked Flur University of Cambridge, Kathryn E. Gray University of Cambridge, Christopher Pulte University of Cambridge, Susmit Sarkar University of St Andrews, Luc Maranget INRIA Rocquencourt, Ali Sezgin University of Cambridge, Will Deacon ARM Ltd., Peter Sewell University of Cambridge
Media Attached File Attached
10:55
25m
Talk
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Research Papers
Jean Pichon-Pharabod University of Cambridge, Peter Sewell University of Cambridge
File Attached
11:20
25m
Talk
Overhauling SC atomics in C11 and OpenCL
Research Papers
John Wickerson Imperial College London, Mark Batty University of Cambridge, Alastair F. Donaldson Imperial College London
Pre-print File Attached
11:45
25m
Talk
Taming Release-Acquire Consistency
Research Papers
Ori Lahav MPI-SWS, Nick Giannarakis MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Pre-print Media Attached File Attached
14:20 - 16:00
Track 1: SynthesisResearch Papers at Grand Bay North
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:20
25m
Talk
Learning Programs from Noisy Data
Research Papers
Veselin Raychev ETH Zurich, Pavol Bielik ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Andreas Krause ETH Zurich
Link to publication DOI Pre-print Media Attached File Attached
14:45
25m
Talk
Optimizing Synthesis with Metasketches
Research Papers
James Bornholt University of Washington, Emina Torlak University of Washington, Dan Grossman University of Washington, USA, Luis Ceze University of Washington, USA
Pre-print Media Attached
15:10
25m
Talk
Maximal Specification Synthesis
Research Papers
Aws Albarghouthi University of Wisconsin–Madison, Işıl Dillig University of Texas, Austin, Arie Gurfinkel Carnegie Mellon University
Pre-print Media Attached
15:35
25m
Talk
Example-Directed Synthesis: A Type-Theoretic Interpretation
Research Papers
Jonathan Frankle Princeton University, Peter-Michael Osera Grinnell College, David Walker Princeton University, Steve Zdancewic University of Pennsylvania
Pre-print Media Attached File Attached
14:20 - 15:35
Track 2: Foundations of Model CheckingResearch Papers at Grand Bay South
Chair(s): Alexandra Silva Radboud University Nijmegen
14:20
25m
Talk
Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
Research Papers
Ichiro Hasuo University of Tokyo, Shunsuke Shimizu University of Tokyo, Corina Cirstea University of Southampton
Media Attached
14:45
25m
Talk
Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
Research Papers
Media Attached
15:10
25m
Talk
Memoryful Geometry of Interaction II: Recursion and Adequacy
Research Papers
Koko Muroya University of Tokyo, Naohiko Hoshino Kyoto University, Ichiro Hasuo University of Tokyo
Media Attached

Accepted Papers

Title
Abstracting Gradual Typing
Research Papers
Link to publication Media Attached
Abstraction Refinement Guided by a Learnt Probabilistic Model
Research Papers
Media Attached
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Research Papers
File Attached
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
Research Papers
Media Attached
Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
Research Papers
Media Attached
A Program Logic for Concurrent Objects under Fair Scheduling
Research Papers
Media Attached
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Research Papers
Binding as Sets of Scopes
Research Papers
Pre-print Media Attached
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
Research Papers
Media Attached File Attached
Casper: An Efficient Approach to Call Trace Collection
Research Papers
Media Attached
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Research Papers
Media Attached
Certified Causally Consistent Distributed Key-Value Stores
Research Papers
Media Attached
Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
Research Papers
Media Attached
Decidability of Inferring Inductive Invariants
Research Papers
Media Attached
Dependent Types and Multi-Monadic Effects in F*
Research Papers
Pre-print Media Attached
Effects as sessions, sessions as effects
Research Papers
Pre-print Media Attached
Environmental Bisimulations for Probabilistic Higher-Order Languages
Research Papers
Media Attached
Estimating types in binaries using predictive modeling
Research Papers
Media Attached File Attached
Example-Directed Synthesis: A Type-Theoretic Interpretation
Research Papers
Pre-print Media Attached File Attached
Fabular: Regression Formulas as Probabilistic Programming
Research Papers
Media Attached
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Media Attached
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Pre-print Media Attached
Is Sound Gradual Typing Dead?
Research Papers
Pre-print Media Attached File Attached
Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Research Papers
Media Attached
Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
Research Papers
Media Attached
Learning Invariants using Decision Trees and Implication Counterexamples
Research Papers
Media Attached
Learning Programs from Noisy Data
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Lightweight Verification of Separate Compilation
Research Papers
Media Attached File Attached
Maximal Specification Synthesis
Research Papers
Pre-print Media Attached
Memoryful Geometry of Interaction II: Recursion and Adequacy
Research Papers
Media Attached
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Research Papers
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Research Papers
Media Attached File Attached
Monitors and Blame Assignment for Higher-Order Session Types
Research Papers
Media Attached File Attached
Newtonian Program Analysis via Tensor Product
Research Papers
Media Attached
Optimizing Synthesis with Metasketches
Research Papers
Pre-print Media Attached
Overhauling SC atomics in C11 and OpenCL
Research Papers
Pre-print File Attached
PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs
Research Papers
Media Attached
Principal Type Inference for GADTs
Research Papers
Media Attached
Printing Floating-Point Numbers: A Faster, Always Correct Method
Research Papers
Media Attached
Prophet: Automatic Patch Generation via Learning from Successful Patches
Research Papers
Media Attached
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
Pushdown Control-flow Analysis for Free
Research Papers
Pre-print Media Attached
Query-Guided Maximum Satisfiability
Research Papers
File Attached
Reducing Crash Recoverability to Reachability
Research Papers
Scaling Network Verification using Symmetry and Surgery
Research Papers
Pre-print
SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization
Research Papers
Media Attached File Attached
Sound Type-dependent Syntactic Language Extension
Research Papers
Pre-print Media Attached File Attached
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
Research Papers
Media Attached
Symbolic Abstract Data Type Inference
Research Papers
Media Attached
Symbolic Computation of Differential Equivalences
Research Papers
Media Attached
System Fω with Equirecursive Types for Datatype-generic Programming
Research Papers
Media Attached
Taming Release-Acquire Consistency
Research Papers
Pre-print Media Attached File Attached
Temporal Verification of Higher-order Functional Programs
Research Papers
The Complexity of Interaction
Research Papers
Media Attached
The Gradualizer: a methodology and algorithm for generating gradual type systems
Research Papers
Media Attached
The Hardness of Data Packing
Research Papers
Media Attached
Transforming Spreadsheet Data Types using Examples
Research Papers
Media Attached
Type Theory in Type Theory using Quotient Inductive Types
Research Papers
Media Attached File Attached
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
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 period17 September, 12:00 noon CET - 20 September, 11:00pm CET
Author notification05 October 2015
Camera-ready deadline05 November 2015
Main conference20-22 January 2016
Co-located events17-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:

  1. author names and institutions must be omitted, and
  2. 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. David Walker has put together a document answering frequently asked questions that should address many common concerns.

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.

POPL 2016- Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Full Citation in the ACM Digital Library

SESSION: Keynotes

Programming the world of uncertain things (keynote)

  • Kathryn S. McKinley

Synthesis of reactive controllers for hybrid systems (keynote)

  • Richard M. Murray

Confluences in programming languages research (keynote)

  • David Walker

SESSION: Types and Foundations

Breaking through the normalization barrier: a self-interpreter for f-omega

  • Matt Brown
  • Jens Palsberg

Type theory in type theory using quotient inductive types

  • Thorsten Altenkirch
  • Ambrus Kaposi

System f-omega with equirecursive types for datatype-generic programming

  • Yufei Cai
  • Paolo G. Giarrusso
  • Klaus Ostermann

A theory of effects and resources: adjunction models and polarised calculi

  • Pierre-Louis Curien
  • Marcelo Fiore
  • Guillaume Munch-Maccagnoni

SESSION: Algorithmic Verification

Temporal verification of higher-order functional programs

  • Akihiro Murase
  • Tachio Terauchi
  • Naoki Kobayashi
  • Ryosuke Sato
  • Hiroshi Unno

Scaling network verification using symmetry and surgery

  • Gordon D. Plotkin
  • Nikolaj Bjørner
  • Nuno P. Lopes
  • Andrey Rybalchenko
  • George Varghese

Model checking for symbolic-heap separation logic with inductive predicates

  • James Brotherston
  • Nikos Gorogiannis
  • Max Kanovich
  • Reuben Rowe

Reducing crash recoverability to reachability

  • Eric Koskinen
  • Junfeng Yang

SESSION: Decision Procedures

Query-guided maximum satisfiability

  • Xin Zhang
  • Ravi Mangal
  • Aditya V. Nori
  • Mayur Naik

String solving with word equations and transducers: towards a logic for analysing mutation XSS

  • Anthony W. Lin
  • Pablo Barceló

Symbolic computation of differential equivalences

  • Luca Cardelli
  • Mirco Tribastone
  • Max Tschaikowski
  • Andrea Vandin

Unboundedness and downward closures of higher-order pushdown automata

  • Matthew Hague
  • Jonathan Kochems
  • C.-H. Luke Ong

SESSION: Correct Compilation

Fully-abstract compilation by approximate back-translation

  • Dominique Devriese
  • Marco Patrignani
  • Frank Piessens

Lightweight verification of separate compilation

  • Jeehoon Kang
  • Yoonseung Kim
  • Chung-Kil Hur
  • Derek Dreyer
  • Viktor Vafeiadis

From MinX to MinC: semantics-driven decompilation of recursive datatypes

  • Ed Robbins
  • Andy King
  • Tom Schrijvers

Sound type-dependent syntactic language extension

  • Florian Lorenzen
  • Sebastian Erdweg

SESSION: Decidability and Complexity

Decidability of inferring inductive invariants

  • Oded Padon
  • Neil Immerman
  • Sharon Shoham
  • Aleksandr Karbyshev
  • Mooly Sagiv

The hardness of data packing

  • Rahman Lavaee

The complexity of interaction

  • Stéphane Gimenez
  • Georg Moser

SESSION: Language Design

Dependent types and multi-monadic effects in F*

  • Nikhil Swamy
  • Cătălin Hriţcu
  • Chantal Keller
  • Aseem Rastogi
  • Antoine Delignat-Lavaud
  • Simon Forest
  • Karthikeyan Bhargavan
  • Cédric Fournet
  • Pierre-Yves Strub
  • Markulf Kohlweiss
  • Jean-Karim Zinzindohoue
  • Santiago Zanella-Béguelin

Fabular: regression formulas as probabilistic programming

  • Johannes Borgström
  • Andrew D. Gordon
  • Long Ouyang
  • Claudio Russo
  • Adam Ścibior
  • Marcin Szymczak

Kleenex: compiling nondeterministic transducers to deterministic streaming transducers

  • Bjørn Bugge Grathwohl
  • Fritz Henglein
  • Ulrik Terp Rasmussen
  • Kristoffer Aalund Søholm
  • Sebastian Paaske Tørholm

SESSION: Probabilistic and Statistical Analysis

Automatic patch generation by learning correct code

  • Fan Long
  • Martin Rinard

Estimating types in binaries using predictive modeling

  • Omer Katz
  • Ran El-Yaniv
  • Eran Yahav

Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs

  • Krishnendu Chatterjee
  • Hongfei Fu
  • Petr Novotný
  • Rouzbeh Hasheminezhad

Transforming spreadsheet data types using examples

  • Rishabh Singh
  • Sumit Gulwani

SESSION: Foundations of Distributed Systems

Chapar: certified causally consistent distributed key-value stores

  • Mohsen Lesani
  • Christian J. Bell
  • Adam Chlipala

'Cause i'm strong enough: reasoning about consistency choices in distributed systems

  • Alexey Gotsman
  • Hongseok Yang
  • Carla Ferreira
  • Mahsa Najafzadeh
  • Marc Shapiro

A program logic for concurrent objects under fair scheduling

  • Hongjin Liang
  • Xinyu Feng

PSync: a partially synchronous language for fault-tolerant distributed algorithms

  • Cezara Drăgoi
  • Thomas A. Henzinger
  • Damien Zufferey

SESSION: Types, Generally or Gradually

Principal type inference for GADTs

  • Sheng Chen
  • Martin Erwig

Abstracting gradual typing

  • Ronald Garcia
  • Alison M. Clark
  • Éric Tanter

The gradualizer: a methodology and algorithm for generating gradual type systems

  • Matteo Cimini
  • Jeremy G. Siek

Is sound gradual typing dead?

  • Asumu Takikawa
  • Daniel Feltey
  • Ben Greenman
  • Max S. New
  • Jan Vitek
  • Matthias Felleisen

SESSION: Learning and Verification

Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis

  • Damien Octeau
  • Somesh Jha
  • Matthew Dering
  • Patrick McDaniel
  • Alexandre Bartel
  • Li Li
  • Jacques Klein
  • Yves Le Traon

Abstraction refinement guided by a learnt probabilistic model

  • Radu Grigore
  • Hongseok Yang

Learning invariants using decision trees and implication counterexamples

  • Pranav Garg
  • Daniel Neider
  • P. Madhusudan
  • Dan Roth

Symbolic abstract data type inference

  • Michael Emmi
  • Constantin Enea

SESSION: Optimization

SMO: an integrated approach to intra-array and inter-array storage optimization

  • Somashekaracharya G. Bhaskaracharya
  • Uday Bondhugula
  • Albert Cohen

PolyCheck: dynamic verification of iteration space transformations on affine programs

  • Wenlei Bao
  • Sriram Krishnamoorthy
  • Louis-Noël Pouchet
  • Fabrice Rastello
  • P. Sadayappan

Printing floating-point numbers: a faster, always correct method

  • Marc Andrysco
  • Ranjit Jhala
  • Sorin Lerner

SESSION: Sessions and Processes

Effects as sessions, sessions as effects

  • Dominic Orchard
  • Nobuko Yoshida

Monitors and blame assignment for higher-order session types

  • Limin Jia
  • Hannah Gommerstadt
  • Frank Pfenning

Environmental bisimulations for probabilistic higher-order languages

  • Davide Sangiorgi
  • Valeria Vignudelli

SESSION: Semantics and Memory Models

Modelling the ARMv8 architecture, operationally: concurrency and ISA

  • Shaked Flur
  • Kathryn E. Gray
  • Christopher Pulte
  • Susmit Sarkar
  • Ali Sezgin
  • Luc Maranget
  • Will Deacon
  • Peter Sewell

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

  • Jean Pichon-Pharabod
  • Peter Sewell

Overhauling SC atomics in c11 and OpenCL

  • Mark Batty
  • Alastair F. Donaldson
  • John Wickerson

Taming release-acquire consistency

  • Ori Lahav
  • Nick Giannarakis
  • Viktor Vafeiadis

SESSION: Program Design and Analysis

Newtonian program analysis via tensor product

  • Thomas Reps
  • Emma Turetsky
  • Prathmesh Prabhu

Casper: an efficient approach to call trace collection

  • Rongxin Wu
  • Xiao Xiao
  • Shing-Chi Cheung
  • Hongyu Zhang
  • Charles Zhang

Pushdown control-flow analysis for free

  • Thomas Gilray
  • Steven Lyde
  • Michael D. Adams
  • Matthew Might
  • David Van Horn

Binding as sets of scopes

  • Matthew Flatt

SESSION: Foundations of Model Checking

Lattice-theoretic progress measures and coalgebraic model checking

  • Ichiro Hasuo
  • Shunsuke Shimizu
  • Corina Cîrstea

Algorithms for algebraic path properties in concurrent systems of constant treewidth components

  • Krishnendu Chatterjee
  • Amir Kafshdar Goharshady
  • Rasmus Ibsen-Jensen
  • Andreas Pavlogiannis

Memoryful geometry of interaction II: recursion and adequacy

  • Koko Muroya
  • Naohiko Hoshino
  • Ichiro Hasuo

SESSION: Synthesis

Learning programs from noisy data

  • Veselin Raychev
  • Pavol Bielik
  • Martin Vechev
  • Andreas Krause

Optimizing synthesis with metasketches

  • James Bornholt
  • Emina Torlak
  • Dan Grossman
  • Luis Ceze

Maximal specification synthesis

  • Aws Albarghouthi
  • Isil Dillig
  • Arie Gurfinkel

Example-directed synthesis: a type-theoretic interpretation

  • Jonathan Frankle
  • Peter-Michael Osera
  • David Walker
  • Steve Zdancewic