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


Title Page


Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher ORCID logo, Benjamin C. PierceORCID logo, David Walker ORCID logo, and Steve ZdancewicORCID logo
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)
Artifacts Functional
WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala and Rishabh Singh
(Massachusetts Institute of Technology, USA; Microsoft Research, USA)
Artifacts Functional
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague ORCID logo, Anthony W. Lin, and Zhilin Wu ORCID logo
(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)
String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš HolíkORCID logo, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš VojnarORCID logo
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)
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 ORCID logo
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)
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)
Handling Fibred Algebraic Effects
Danel Ahman
(Inria, France)
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki ORCID logo, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Info Artifacts Functional


Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan ChinORCID logo
(National University of Singapore, Singapore)
Info Artifacts Functional
Foundations for Natural Proofs and Quantifier Instantiation
Christof Löding, P. MadhusudanORCID logo, and Lucas Peña ORCID logo
(RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA)
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)
Artifacts Functional
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Hiroshi UnnoORCID logo, Yuki Satake, and Tachio Terauchi ORCID logo
(University of Tsukuba, Japan; Waseda University, Japan)

Interpretation and Evaluation

Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux ORCID logo, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland; University of Pennsylvania, USA)
Artifacts Functional
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Matt Brown and Jens PalsbergORCID logo
(University of California at Los Angeles, USA)
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)
Artifacts Functional
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen ORCID logo, Arjen Rouvoet ORCID logo, Andrew Tolmach, Robbert KrebbersORCID logo, and Eelco Visser ORCID logo
(Delft University of Technology, Netherlands; Portland State University, USA)
Artifacts Functional

Memory and Concurrency

Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori LahavORCID logo, Konstantinos Sagonas ORCID logo, and Viktor VafeiadisORCID logo
(National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany)
Info Artifacts Functional
Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, and James Riely
(Brunel University London, UK; DePaul University, USA)
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher PulteORCID logo, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell ORCID logo
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
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)


A Principled Approach to Ornamentation in ML
Thomas Williams and Didier RémyORCID logo
(Inria, France)
Info Artifacts Functional
Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible
William J. Bowman ORCID logo, Youyou Cong, Nick Rioux, and Amal AhmedORCID logo
(Northeastern University, USA; Ochanomizu University, Japan)
Decidability of Conversion for Type Theory in Type Theory
Andreas Abel ORCID logo, Joakim Öhman ORCID logo, and Andrea Vezzosi
(University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden)
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)


Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Michael Emmi and Constantin Enea
(SRI International, USA; University of Paris Diderot, France; CNRS, France)
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski ORCID logo, Mooly Sagiv ORCID logo, and Sharon Shoham ORCID logo
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Info Artifacts Functional
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan ORCID logo
(Purdue University, USA)
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, and Zachary Tatlock ORCID logo
(University College London, UK; University of Washington, USA)
Info 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 ORCID logo
(Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil)
Info Artifacts Functional
Optimal Dyck Reachability for Data-Dependence and Alias Analysis
Krishnendu Chatterjee ORCID logo, Bhavya Choudhary, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Artifacts Functional
Data-Centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee ORCID logo, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya
(Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
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)


A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen ORCID logo
(Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee ORCID logo, and Petr Novotný
(IIT Bombay, India; IST Austria, Austria)
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)
Monadic Refinements for Relational Cost Analysis
Ivan Radiček, Gilles Barthe ORCID logo, Marco Gaboardi, Deepak GargORCID logo, and Florian Zuleger
(Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)

Outside the Box

Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, and Thomas Wies ORCID logo
(New York University, USA)
Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
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)
Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, and Emina Torlak
(Northeastern University, USA; University of Washington, USA)
Artifacts Functional

Language Design

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

Dependent Types

Up-to Techniques using Sized Types
Nils Anders Danielsson ORCID logo
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)
Artifacts Functional
Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti and Nicolai Kraus
(University of Nottingham, UK)
Info Artifacts Functional

Testing and Verification

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

Dynamic Languages

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

Program Analysis

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


Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe ORCID logo, Thomas Espitau, Benjamin Grégoire ORCID logo, Justin HsuORCID logo, and Pierre-Yves Strub ORCID logo
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)
Artifacts Functional
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi ORCID logo and Justin HsuORCID logo
(University of Wisconsin-Madison, USA; University College London, UK)
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)
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam StatonORCID logo, Hongseok YangORCID logo, Yufei Cai, Klaus Ostermann ORCID logo, Sean K. Moss, Chris Heunen ORCID logo, 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)


Strategy Synthesis for Linear Arithmetic Games
Azadeh FarzanORCID logo and Zachary Kincaid ORCID logo
(University of Toronto, Canada; Princeton University, USA)
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)
Artifacts Functional
Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig ORCID logo, and Rishabh Singh
(University of Texas at Austin, USA; Microsoft Research, USA)

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 BirkedalORCID logo
(KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark)
Artifacts Functional
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet ORCID logo, Cătălin Hriţcu, Kenji Maillard ORCID logo, Aseem Rastogi ORCID logo, and Nikhil Swamy ORCID logo
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Info Artifacts Functional
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf JungORCID logo, Jacques-Henri Jourdan, Robbert KrebbersORCID logo, and Derek DreyerORCID logo
(MPI-SWS, Germany; Delft University of Technology, Netherlands)
Info Artifacts Functional

proc time: 0.15