POPL 2017

1 Name: Anonymous 2017-04-23 16:53
It's that time of year again, Principles of Programming Languages papers released. Let's see what's worth reading..

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

A Program Optimization for Automatic Database Result Caching
Ziv Scully, Adam Chlipala

A Promising Semantics for Relaxed-Memory Concurrency
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
Link to publication Pre-print Media Attached

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

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

A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder
DOI Pre-print

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

Automatically Comparing Memory Consistency Models
John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides
Pre-print Media Attached File Attached

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

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

Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
Michael Vitousek, Cameron Swords, Jeremy Siek

Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva
DOI File Attached

Coming to Terms with Quantified Reasoning
Simon Robillard, Andrei Voronkov, Laura Kovacs

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

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

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

Contextual isomorphisms
Paul Blain Levy

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

Coupling proofs are probabilistic product programs
Gilles Barthe, Benjamin Gregoire, Justin Hsu, Pierre-Yves Strub

Deciding equivalence with sums and the empty type
Gabriel Scherer

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

Do be do be do
Sam Lindley, Conor McBride, Craig McLaughlin

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

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

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

Fencing off Go: Liveness and Safety for Channel-Based Programming
Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida

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

Gradual Refinement Types
Nicolás Lehmann, Éric Tanter
Link to publication DOI Pre-print

Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew Hammer

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

Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany, Lars Birkedal
DOI Pre-print Media Attached

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

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

LOIS: syntax and semantics
Eryk Kopczynski, Szymon Toruńczyk

Learning nominal automata
Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, Michał Szynwelski

LightDP: Towards Automating Differential Privacy Proofs
Danfeng Zhang, Daniel Kifer

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

Modules, Abstraction, and Parametric Polymorphism
Karl Crary

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

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

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

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

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

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

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

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

Stateful Manifest Contracts
Taro Sekiyama, Atsushi Igarashi

Stochastic Invariants for Probabilistic Termination
Krishnendu Chatterjee, Petr Novotny, Djordje Zikelic

Stream Fusion, to Completeness
Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis
Pre-print Media Attached

Sums of Uncertainty: Refinements go gradual
Khurram A. Jafery, Joshua Dunfield

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

The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
Danko Ilik

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

Type Directed Compilation of Row-Typed Algebraic Effects
Daan Leijen

Type Soundness Proofs with Definitional Interpreters
Nada Amin, Tiark Rompf

Type Systems as Macros
Stephen Chang, Alex Knauth, Ben Greenman

Typed Self-Evaluation via Intensional Type Functions
Matt Brown, Jens Palsberg
2 Name: Anonymous 2017-04-23 16:57
Not a single interesting paper, not even the one with olegs name on it is worth reading.

Leave this field blank: