POPL 2018
Proceedings of the ACM on Programming Languages, Volume 2, Number POPL
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 2, Number POPL, January 7–13, 2018, Los Angeles, CA, USA

POPL – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page

Strings

Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)
Preprint Archive submitted (24 MB) Artifacts Available Artifacts Functional
WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala and Rishabh Singh
(Massachusetts Institute of Technology, USA; Microsoft Research, USA)
Article Search Artifacts Functional
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
(University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
Article Search
String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)
Preprint Info Artifacts Functional

Types and Effects 1

Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)
Article Search Artifacts Functional
Polyadic Approximations, Fibrations and Intersection Types
Damiano Mazza, Luc Pellissier, and Pierre Vial
(CNRS, France; University of Paris 13, France; University of Paris Diderot, France)
Article Search
Handling Fibred Algebraic Effects
Danel Ahman
(Inria, France)
Article Search
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Article Search Archive submitted (0 MB) Info Artifacts Available Artifacts Functional

Verification

Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Preprint Archive submitted (9 MB) Info Artifacts Available Artifacts Functional
Foundations for Natural Proofs and Quantifier Instantiation
Christof Löding, P. Madhusudan, and Lucas Peña
(RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA)
Article Search Archive submitted (0 MB) Artifacts Available Artifacts Functional
Higher-Order Constrained Horn Clauses for Verification
Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay
(University of Oxford, UK; University of Bristol, UK)
Article Search Artifacts Functional
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Hiroshi Unno, Yuki Satake, and Tachio Terauchi
(University of Tsukuba, Japan; Waseda University, Japan)
Article Search

Interpretation and Evaluation

Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland; University of Pennsylvania, USA)
Article Search Artifacts Functional
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)
Article Search Info Artifacts Functional
Migrating Gradual Types
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)
Article Search Archive submitted (0 MB) Artifacts Available Artifacts Functional
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Portland State University, USA)
Article Search Archive submitted (1 MB) Artifacts Available Artifacts Functional

Memory and Concurrency

Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis
(National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany)
Preprint Archive submitted (2232 MB) Info Artifacts Available Artifacts Functional
Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, and James Riely
(Brunel University London, UK; DePaul University, USA)
Preprint
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
Article Search Artifacts Functional
Progress of Concurrent Objects with Partial Methods
Hongjin Liang and Xinyu Feng
(Nanjing University, China; University of Science and Technology of China, China)
Article Search

Types

A Principled Approach to Ornamentation in ML
Thomas Williams and Didier Rémy
(Inria, France)
Article Search Info Artifacts Functional
Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible
William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed
(Northeastern University, USA; Ochanomizu University, Japan)
Preprint Archive submitted (1 MB) Info
Decidability of Conversion for Type Theory in Type Theory
Andreas Abel, Joakim Öhman, and Andrea Vezzosi
(University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden)
Article Search Artifacts Functional
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Ondřej Kunčar and Andrei Popescu
(TU Munich, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania)
Preprint Info

Consistency

Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Michael Emmi and Constantin Enea
(SRI International, USA; University of Paris Diderot, France; CNRS, France)
Article Search
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Article Search Archive submitted (3466 MB) Info Artifacts Available Artifacts Functional
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan
(Purdue University, USA)
Article Search
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, and Zachary Tatlock
(University College London, UK; University of Washington, USA)
Preprint Archive submitted (0 MB) Info Artifacts Available Artifacts Functional

Types and Effects 2

Inference of Static Semantics for Incomplete C Programs
Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil)
Preprint Archive submitted (9 MB) Info Artifacts Available Artifacts Functional
Optimal Dyck Reachability for Data-Dependence and Alias Analysis
Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Article Search Artifacts Functional
Data-Centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya
(Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
Article Search
Analytical Modeling of Cache Behavior for Affine Programs
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan
(Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
Article Search

Termination

A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen
(Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
Article Search
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný
(IIT Bombay, India; IST Austria, Austria)
Article Search Artifacts Functional
Algorithmic Analysis of Termination Problems for Quantum Programs
Yangjia Li and Mingsheng Ying
(Institute of Software at Chinese Academy of Sciences, China; University of Technology Sydney, Australia; Tsinghua University, China)
Article Search
Monadic Refinements for Relational Cost Analysis
Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger
(Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
Article Search

Outside the Box

Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, and Thomas Wies
(New York University, USA)
Article Search
Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
Article Search Archive submitted (0 MB)
Linearity in Higher-Order Recursion Schemes
Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Inria, France; Aix-Marseille University, France; ENSAM, France; University of Toulon, France; University of Oxford, UK)
Article Search
Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, and Emina Torlak
(Northeastern University, USA; University of Washington, USA)
Article Search Artifacts Functional

Language Design

An Axiomatic Basis for Bidirectional Programming
Hsiang-Shang Ko and Zhenjiang Hu
(National Institute of Informatics, Japan)
Preprint Archive submitted (2 MB) Info Artifacts Available Artifacts Functional
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)
Article Search Archive submitted (0 MB) Artifacts Available Artifacts Functional

Dependent Types

Up-to Techniques using Sized Types
Nils Anders Danielsson
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)
Article Search Archive submitted (2 MB) Artifacts Available Artifacts Functional
Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti and Nicolai Kraus
(University of Nottingham, UK)
Preprint Info Artifacts Functional

Testing and Verification

Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce
(University of Pennsylvania, USA; Princeton University, USA)
Article Search Info Artifacts Functional
Why Is Random Testing Effective for Partition Tolerance Bugs?
Rupak Majumdar and Filip Niksic
(MPI-SWS, Germany)
Article Search
On Automatically Proving the Correctness of math.h Implementations
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India)
Article Search
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Article Search Artifacts Functional

Dynamic Languages

Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek
(Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
Preprint
JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Article Search Archive submitted (2813 MB) Artifacts Available Artifacts Functional
Soft Contract Verification for Higher-Order Stateful Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland, USA; Indiana University, USA)
Preprint Archive submitted (7 MB) Info Artifacts Available Artifacts Functional
Collapsing Towers of Interpreters
Nada Amin and Tiark Rompf
(University of Cambridge, UK; Purdue University, USA)
Article Search Info Artifacts Functional

Program Analysis

Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Article Search Archive submitted (54 MB) Artifacts Available Artifacts Functional
Non-linear Reasoning for Invariant Synthesis
Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps
(Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA)
Article Search Archive submitted (3187 MB) Artifacts Available Artifacts Functional
A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Article Search Info Artifacts Functional
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook
(University of Texas at Austin, USA; Microsoft Research, USA)
Article Search

Probability

Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)
Preprint Artifacts Functional
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi and Justin Hsu
(University of Wisconsin-Madison, USA; University College London, UK)
Preprint
Measurable Cones and Stable, Measurable Functions: A Model for Probabilistic Higher-Order Programming
Thomas Ehrhard, Michele Pagani, and Christine Tasson
(University of Paris Diderot, France; CNRS, France)
Article Search Info
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Article Search Info

Synthesis

Strategy Synthesis for Linear Arithmetic Games
Azadeh Farzan and Zachary Kincaid
(University of Toronto, Canada; Princeton University, USA)
Article Search Archive submitted (2829 MB) Artifacts Available Artifacts Functional
Bonsai: Synthesis-Based Reasoning for Type Systems
Kartik Chandra and Rastislav Bodik
(Henry M. Gunn High School, USA; Stanford University, USA; University of Washington, USA)
Article Search Artifacts Functional
Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig, and Rishabh Singh
(University of Texas at Austin, USA; Microsoft Research, USA)
Article Search

Types for State

A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal
(KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark)
Article Search Archive submitted (1 MB) Artifacts Available Artifacts Functional
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Preprint Archive submitted (0 MB) Info Artifacts Available Artifacts Functional
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer
(MPI-SWS, Germany; Delft University of Technology, Netherlands)
Preprint Archive submitted (0 MB) Info Artifacts Available Artifacts Functional

proc time: 5.38