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

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

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

Save

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 James Brotherston , Nikos Gorogiannis , Max Kanovich , Reuben Rowe
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	BanquetResearch Papers at Dali Museum

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 Mohsen Lesani MIT, Christian J. Bell MIT CSAIL, Adam Chlipala MIT 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 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, Isil 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 Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady , Rasmus Ibsen-Jensen , Andreas Pavlogiannis 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 Ronald Garcia, Alison M. Clark, Éric Tanter Link to publication Media Attached
	Abstraction Refinement Guided by a Learnt Probabilistic Model Research Papers Radu Grigore, Hongseok Yang Media Attached
	A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions Research Papers Jean Pichon-Pharabod, Peter Sewell File Attached
	Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs Research Papers Krishnendu Chatterjee, Hongfei Fu, Rouzbeh Hasheminezhad, Petr Novotný Media Attached
	Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components Research Papers Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis Media Attached
	A Program Logic for Concurrent Objects under Fair Scheduling Research Papers Hongjin Liang, Xinyu Feng Media Attached
	A Theory of Effects and Resources: Adjunction Models and Polarised Calculi Research Papers Pierre-Louis Curien, Marcelo Fiore, Guillaume Munch-Maccagnoni
	Binding as Sets of Scopes Research Papers Matthew Flatt Pre-print Media Attached
	Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega Research Papers Matt Brown, Jens Palsberg Media Attached File Attached
	Casper: An Efficient Approach to Call Trace Collection Research Papers Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang Media Attached
	'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems Research Papers Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro Media Attached
	Certified Causally Consistent Distributed Key-Value Stores Research Papers Mohsen Lesani, Christian J. Bell, Adam Chlipala Media Attached
	Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis Research Papers Damien Octeau, Somesh Jha, Matthew Dering, Patrick McDaniel, Alexandre Bartel, Hongyu Li, Jacques Klein, Yves Le Traon Media Attached
	Decidability of Inferring Inductive Invariants Research Papers Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv Media Attached
	Dependent Types and Multi-Monadic Effects in F* Research Papers 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 Zinzindohoué, Santiago Zanella-Béguelin Pre-print Media Attached
	Effects as sessions, sessions as effects Research Papers Dominic Orchard, Nobuko Yoshida Pre-print Media Attached
	Environmental Bisimulations for Probabilistic Higher-Order Languages Research Papers Davide Sangiorgi, Valeria Vignudelli Media Attached
	Estimating types in binaries using predictive modeling Research Papers Omer Katz, Ran El-Yaniv, Eran Yahav Media Attached File Attached
	Example-Directed Synthesis: A Type-Theoretic Interpretation Research Papers Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic Pre-print Media Attached File Attached
	Fabular: Regression Formulas as Probabilistic Programming Research Papers Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio Russo, Adam Ścibior, Marcin Szymczak Media Attached
	From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes Research Papers Ed Robbins, Andy King, Tom Schrijvers Media Attached
	Fully-Abstract Compilation by Approximate Back-Translation Research Papers Dominique Devriese, Marco Patrignani, Frank Piessens Pre-print Media Attached
	Is Sound Gradual Typing Dead? Research Papers Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, Matthias Felleisen Pre-print Media Attached File Attached
	Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers Research Papers Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm Media Attached
	Lattice-Theoretic Progress Measures and Coalgebraic Model Checking Research Papers Ichiro Hasuo, Shunsuke Shimizu, Corina Cirstea Media Attached
	Learning Invariants using Decision Trees and Implication Counterexamples Research Papers Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth Media Attached
	Learning Programs from Noisy Data Research Papers Veselin Raychev, Pavol Bielik, Martin Vechev, Andreas Krause Link to publication DOI Pre-print Media Attached File Attached
	Lightweight Verification of Separate Compilation Research Papers Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis Media Attached File Attached
	Maximal Specification Synthesis Research Papers Aws Albarghouthi, Isil Dillig, Arie Gurfinkel Pre-print Media Attached
	Memoryful Geometry of Interaction II: Recursion and Adequacy Research Papers Koko Muroya, Naohiko Hoshino, Ichiro Hasuo Media Attached
	Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates Research Papers James Brotherston, Nikos Gorogiannis, Max Kanovich, Reuben Rowe
	Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA Research Papers Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Luc Maranget, Ali Sezgin, Will Deacon, Peter Sewell Media Attached File Attached
	Monitors and Blame Assignment for Higher-Order Session Types Research Papers Limin Jia, Hannah Gommerstadt, Frank Pfenning Media Attached File Attached
	Newtonian Program Analysis via Tensor Product Research Papers Thomas Reps, Emma Turetsky, Prathmesh Prabhu Media Attached
	Optimizing Synthesis with Metasketches Research Papers James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze Pre-print Media Attached
	Overhauling SC atomics in C11 and OpenCL Research Papers John Wickerson, Mark Batty, Alastair F. Donaldson Pre-print File Attached
	PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs Research Papers Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, P. Sadayappan Media Attached
	Principal Type Inference for GADTs Research Papers Sheng Chen, Martin Erwig Media Attached
	Printing Floating-Point Numbers: A Faster, Always Correct Method Research Papers Marc Andrysco, Ranjit Jhala, Sorin Lerner Media Attached
	Prophet: Automatic Patch Generation via Learning from Successful Patches Research Papers Fan Long, Martin C. Rinard Media Attached
	PSync: a partially synchronous language for fault-tolerant distributed algorithms Research Papers Cezara Drăgoi, Thomas A. Henzinger, Damien Zufferey Link to publication DOI Pre-print Media Attached File Attached
	Pushdown Control-flow Analysis for Free Research Papers Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn Pre-print Media Attached
	Query-Guided Maximum Satisfiability Research Papers Xin Zhang, Ravi Mangal, Aditya Nori, Mayur Naik File Attached
	Reducing Crash Recoverability to Reachability Research Papers Eric Koskinen, Junfeng Yang
	Scaling Network Verification using Symmetry and Surgery Research Papers Gordon Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese Pre-print
	SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization Research Papers Somashekaracharya G Bhaskaracharya, Uday Bondhugula, Albert Cohen Media Attached File Attached
	Sound Type-dependent Syntactic Language Extension Research Papers Florian Lorenzen, Sebastian Erdweg Pre-print Media Attached File Attached
	String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS Research Papers Anthony Widjaja Lin, Pablo Barcelo Media Attached
	Symbolic Abstract Data Type Inference Research Papers Michael Emmi, Constantin Enea Media Attached
	Symbolic Computation of Differential Equivalences Research Papers Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin Media Attached
	System Fω with Equirecursive Types for Datatype-generic Programming Research Papers Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann Media Attached
	Taming Release-Acquire Consistency Research Papers Ori Lahav, Nick Giannarakis, Viktor Vafeiadis Pre-print Media Attached File Attached
	Temporal Verification of Higher-order Functional Programs Research Papers Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
	The Complexity of Interaction Research Papers Stéphane Gimenez, Georg Moser Media Attached
	The Gradualizer: a methodology and algorithm for generating gradual type systems Research Papers Matteo Cimini, Jeremy G. Siek Media Attached
	The Hardness of Data Packing Research Papers Rahman Lavaee, Chen Ding Media Attached
	Transforming Spreadsheet Data Types using Examples Research Papers Rishabh Singh, Sumit Gulwani Media Attached
	Type Theory in Type Theory using Quotient Inductive Types Research Papers Thorsten Altenkirch, Ambrus Kaposi Media Attached File Attached
	Unboundedness and Downward Closures of Higher-Order Pushdown Automata Research Papers Matthew Hague, Jonathan Kochems, C.-H. Luke Ong 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 ...").

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.