popl2017-papers

Links to accepted papers for the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017). Pull requests welcome!

(Similar pages are available for POPL 2016, 2015, 2014, and 2013, ICFP (2016, 2015, 2014, 2013, 2012) and PLDI 2014.)

Note: if you are editing this repository, please remember to use the Markdown syntax for hard line breaks, namely two spaces at the end of the line.

Note: the "final version" deadline for POPL'17 is November 7, so it is fair to assume that more authors will have preprints available after that.

POPL 2017

A Posteriori Environment Analysis with Pushdown Delta CFA
Kimball Germane, Matthew Might
(preprint)

A Program Optimization for Automatic Database Result Caching
Ziv Scully, Adam Chlipala
(website (no preprint yet))

A Promising Semantics for Relaxed-Memory Concurrency
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
(draft, website, coq proofs)

A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal
(preprint)

A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim, Ikram Cherigui, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata
(draft)

A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
(preprint from arXiv)

Analyzing divergence in bisimulation semantics
Xinxin Liu, Tingting Yu, Wenhui Zhang

AutoPriv: Automating Differential Privacy Proofs
Danfeng Zhang, Daniel Kifer
(preprint from arXiv)

Automatically Comparing Memory Consistency Models
John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides
(preprint)

Automatically Generating the Dynamic Semantics of Gradually Typed Languages
Matteo Cimini, Jeremy Siek
(preprint)

Beginner's Luck: A Language for Property-Based Generators
Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Li-yao Xia
(preprint from arXiv)

Big Types in Little Runtime
Michael Vitousek, Cameron Swords, Jeremy Siek

Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva
(preprint from arXiv)

Coming to Terms with Quantified Reasoning
Simon Robillard, Andrei Voronkov, Laura Kovacs
(preprint from arXiv)

Complexity Verification Using Guided Theorem Enumeration
Akhilesh Srikanth, Burak Sahin, William Harris

Component-Based Synthesis for Complex APIs
Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas Reps
(preprint)

Computational Higher-Dimensional Type Theory
Carlo Angiuli, Robert Harper, Todd Wilson
(preprint)

Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
Qirun Zhang, Zhendong Su

Contextual isomorphisms
Paul Blain Levy
(preprint)

Contract-based Resource Verification for Higher-order Functions with Memoization
Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak
(draft)

Coupling proofs are probabilistic product programs
Gilles Barthe, Benjamin Gregoire, Justin Hsu, Pierre-Yves Strub
(preprint from arXiv)

Deciding equivalence with sums and the empty type
Gabriel Scherer
(preprint from arXiv)

Dijkstra Monads for Free
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
(preprint from arXiv, other materials)

Do be do be do
Sam Lindley, Conor McBride, Craig McLaughlin
(preprint from arXiv, slides)

Dynamic Race Detection For C++11
Christopher Lidbury, Alastair Donaldson

Exact Bayesian Inference by Symbolic Disintegration
Chung-chieh Shan, Norman Ramsey
(preprint)

Fast Polyhedra Abstract Domain
Gagandeep Singh, Markus Püschel, Martin Vechev
(preprint)

Fencing off Go: Liveness and Safety for Channel-based Programming
Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida
(preprint from arXiv)

From F to DOT: Type Soundness Proofs with Definitional Interpreters
Nada Amin, Tiark Rompf
(preprint from arXiv)

Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
Kausik Subramanian, Loris D'Antoni, Aditya Akella
(preprint)

Gradual Refinement Types
Nicolás Lehmann, Éric Tanter
(preprint)

Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew Hammer
(preprint from arXiv, website, live implementation, agda proofs)

Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Mounir Assaf, David Naumann, Julien Signoles, Éric Totel, Frédéric Tronel
(preprint from arXiv)

Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany, Lars Birkedal
(preprint)

Intersection Type Calculi of Bounded Dimension
Andrej Dudenhefner, Jakob Rehof

Invariants of Quantum Programs: Characterisations and Generation
Mingsheng Ying, Shenggang Ying, Xiaodi Wu

Java generics are Turing complete
Radu Grigore
(preprint from arXiv)

LMS-Verify: Abstraction Without Regret for Verified Systems Programming
Nada Amin, Tiark Rompf
(draft)

LOIS (Looping Over Infinite Sets): syntax and semantics
Eryk Kopczynski, Szymon Toruńczyk
(preprint)

Learning nominal automata
Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, Michał Szynwelski
(preprint from arXiv)

Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell
(preprint)

Modules, Abstraction, and Parametric Polymorphism
Karl Crary
(preprint)

Monadic second-order logic on finite sequences
Loris D'Antoni, Margus Veanes
(preprint)

Ogre and Pythia, An invariance proof method for weak consistency models
Jade Alglave, Patrick Cousot

On Verifying Causal Consistency
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza
(preprint from arXiv)

On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
Naoki Kobayashi, Etienne Lozes, Florian Bruse

Parallel Functional Arrays
Ananya Kumar, Guy E. Blelloch, Robert Harper
(preprint)

Polymorphism, subtyping and type inference in MLsub
Stephen Dolan, Alan Mycroft
(preprint)

QWIRE: A Core Language for Quantum Circuits
Jennifer Paykin, Robert Rand, Steve Zdancewic
(preprint)

Relational Cost Analysis
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann
(preprint)

Rigorous Floating-point Mixed Precision Tuning
Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Ian Briggs, Mark S. Baranowski, Alexey Solovyev
(implementation)

Semantic-Directed Clumping of Disjunctive Abstract States
Huisong Li, François Bérenger, Bor-Yuh Evan Chang, Xavier Rival

Serializability for Eventual Consistency: Criterion, Analysis and Applications
Lucas Brutschy, Dimitar Dimitrov, Peter Müller, Martin Vechev
(preprint)

Stateful Manifest Contracts
Taro Sekiyama, Atsushi Igarashi
(draft)

Stochastic Invariants for Probabilistic Termination
Krishnendu Chatterjee, Petr Novotny, Djordje Zikelic
(preprint from arXiv)

Stream Fusion, to Completeness
Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis
(preprint, artifact website)

Sums of Uncertainty: Refinements go gradual
Khurram A. Jafery, Joshua Dunfield
(preprint from arXiv)

The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
Ugo Dal Lago, Claudia Faggian, Benoit Valiron, Akira Yoshimizu
(preprint from arXiv)

The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
Danko Ilik
(preprint from arXiv)

Thread Modularity at Many Levels: a Pearl in Compositional Verification
Jochen Hoenicke, Rupak Majumdar, Andreas Podelski

Towards Automatic Resource Bound Analysis for OCaml
Jan Hoffmann, Ankush Das, Shu-Chun Weng
(preprint, long version available on arXiv)

Type Directed Compilation of Row-Typed Algebraic Effects
Daan Leijen
(technical report, website)

Type Systems as Macros
Stephen Chang, Alex Knauth, Ben Greenman
(preprint, website, code repo))

Typed Self-Evaluation via Intensional Type Functions
Matt Brown, Jens Palsberg

Co-located events

As of writing, the submission process for most POPL'17 co-located events is not finished. Feel free to send a pull-request with list of accepted papers for an event, and contribute links to the preprints.

CoqPL 2017

CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani
(preprint)

CertiCoq: A verified compiler for Coq
Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, Matthew Weaver

IxFree: Step-Indexed Logical Relations in Coq
Piotr Polesiuk

Logical Relations in Iris
Amin Timany, Robbert Krebbers, Lars Birkedal
(preprint)

Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting
Edwin Westbrook, Gregory Malecha

Session with the Coq Development Team

Synthetic topology in HoTT for probabilistic programming
Florian Faissole, Bas Spitters

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
Nicolas Magaud

Verification of Implementations of Distributed Systems Under Churn
Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, Karl Palmskog

ppsimpl: a reflexive Coq tactic for canonising goals
Frédéric Besson

PEPM 2017

Papers

A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction
Kazutaka Matsuda, Kazuyuki Asada

Lightweight Soundness for Towers of Language Extensions
Alejandro Serrano, Jurriaan Hage

Predicting Resource Consumption of Higher-Order Workflows
Markus Klinik, Jurriaan Hage, Jan Martin Jansen, Rinus Plasmeijer

Verification of Code Generators via Higher-Order Model Checking
Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi

Refining types using type guards in TypeScript
Ivo Gabe de Wolff, Jurriaan Hage

Cost versus Precision for Approximate Typing for Python
Levin Fritz, Jurriaan Hage

PEG Parsing in Less Space Using Progressive Tabling, Dynamic Analysis
Fritz Henglein, Ulrik Terp Rasmussen
(preprint)

Interactive data representation migration: Exploiting program dependence to aid program transformation
Krishna Narasimhan, Julia Lawall, Christoph Reichenbach

Functional Parallels of Sequential Imperatives (Short Paper)
Tiark Rompf, Kevin J. Brown

Detecting code clones with gaps by function applications
Tsubasa Matsushita, Isao Sasano

Posters

Language-integrated Query with Ordering, Grouping, Outer Joins
Tatsuya Katsushima, Oleg Kiselyov

Study of Bellman Equation from Program Schemata Perspective
Nikolay Shilov