POPL – Journal Issue

Frontmatter

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)

Publisher's Version Artifacts Functional Article: popl18main-p18-p doi:10.1145/3158089

WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala and Rishabh Singh
(Massachusetts Institute of Technology, USA; Microsoft Research, USA)

Publisher's Version Artifacts Functional Article: popl18main-p114-p doi:10.1145/3158090

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)

Publisher's Version Article: popl18main-p264-p doi:10.1145/3158091

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)

Publisher's Version Artifacts Functional Article: popl18main-p266-p doi:10.1145/3158092

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)

Publisher's Version Artifacts Functional Article: popl18main-p2-p doi:10.1145/3158093

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)

Publisher's Version Article: popl18main-p265-p doi:10.1145/3158094

Handling Fibred Algebraic Effects
Danel Ahman
(Inria, France)

Publisher's Version Article: popl18main-p68-p doi:10.1145/3158095

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)

Publisher's Version Artifacts Functional Article: popl18main-p160-p doi:10.1145/3158096

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)

Publisher's Version Artifacts Functional Article: popl18main-p281-p doi:10.1145/3158097

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)

Publisher's Version Artifacts Functional Article: popl18main-p99-p doi:10.1145/3158098

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)

Publisher's Version Artifacts Functional Article: popl18main-p253-p doi:10.1145/3158099

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)

Publisher's Version Article: popl18main-p256-p doi:10.1145/3158100

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)

Publisher's Version Artifacts Functional Article: popl18main-p285-p doi:10.1145/3158101

Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)

Publisher's Version Artifacts Functional Article: popl18main-p189-p doi:10.1145/3158102

Migrating Gradual Types
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)

Publisher's Version Artifacts Functional Article: popl18main-p239-p doi:10.1145/3158103

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)

Publisher's Version Artifacts Functional Article: popl18main-p277-p doi:10.1145/3158104

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)

Publisher's Version Artifacts Functional Article: popl18main-p80-p doi:10.1145/3158105

Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, and James Riely
(Brunel University London, UK; DePaul University, USA)

Publisher's Version Article: popl18main-p154-p doi:10.1145/3158106

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)

Publisher's Version Artifacts Functional Article: popl18main-p5-p doi:10.1145/3158107

Progress of Concurrent Objects with Partial Methods
Hongjin Liang and Xinyu Feng
(Nanjing University, China; University of Science and Technology of China, China)

Publisher's Version Article: popl18main-p96-p doi:10.1145/3158108

Types

A Principled Approach to Ornamentation in ML
Thomas Williams and Didier Rémy
(Inria, France)

Publisher's Version Artifacts Functional Article: popl18main-p200-p doi:10.1145/3158109

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)

Publisher's Version Article: popl18main-p51-p doi:10.1145/3158110

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)

Publisher's Version Artifacts Functional Article: popl18main-p128-p doi:10.1145/3158111

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)

Publisher's Version Article: popl18main-p50-p doi:10.1145/3158112

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)

Publisher's Version Article: popl18main-p59-p doi:10.1145/3158113

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)

Publisher's Version Artifacts Functional Article: popl18main-p145-p doi:10.1145/3158114

Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan
(Purdue University, USA)

Publisher's Version Article: popl18main-p209-p doi:10.1145/3158115

Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, and Zachary Tatlock
(University College London, UK; University of Washington, USA)

Publisher's Version Artifacts Functional Article: popl18main-p115-p doi:10.1145/3158116

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)

Publisher's Version Artifacts Functional Article: popl18main-p110-p doi:10.1145/3158117

Optimal Dyck Reachability for Data-Dependence and Alias Analysis
Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)

Publisher's Version Artifacts Functional Article: popl18main-p187-p doi:10.1145/3158118

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)

Publisher's Version Article: popl18main-p88-p doi:10.1145/3158119

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)

Publisher's Version Article: popl18main-p175-p doi:10.1145/3158120

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)

Publisher's Version Article: popl18main-p53-p doi:10.1145/3158121

Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný
(IIT Bombay, India; IST Austria, Austria)

Publisher's Version Artifacts Functional Article: popl18main-p131-p doi:10.1145/3158122

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)

Publisher's Version Article: popl18main-p47-p doi:10.1145/3158123

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)

Publisher's Version Article: popl18main-p94-p doi:10.1145/3158124

Outside the Box

Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, and Thomas Wies
(New York University, USA)

Publisher's Version Article: popl18main-p190-p doi:10.1145/3158125

Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)

Publisher's Version Article: popl18main-p46-p doi:10.1145/3158126

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)

Publisher's Version Article: popl18main-p178-p doi:10.1145/3158127

Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, and Emina Torlak
(Northeastern University, USA; University of Washington, USA)

Publisher's Version Artifacts Functional Article: popl18main-p180-p doi:10.1145/3158128

Language Design

An Axiomatic Basis for Bidirectional Programming
Hsiang-Shang Ko and Zhenjiang Hu
(National Institute of Informatics, Japan)

Publisher's Version Artifacts Functional Article: popl18main-p3-p doi:10.1145/3158129

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)

Publisher's Version Artifacts Functional Article: popl18main-p247-p doi:10.1145/3158130

Dependent Types

Up-to Techniques using Sized Types
Nils Anders Danielsson
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)

Publisher's Version Artifacts Functional Article: popl18main-p181-p doi:10.1145/3158131

Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti and Nicolai Kraus
(University of Nottingham, UK)

Publisher's Version Artifacts Functional Article: popl18main-p216-p doi:10.1145/3158132

Testing and Verification

Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce
(University of Pennsylvania, USA; Princeton University, USA)

Publisher's Version Artifacts Functional Article: popl18main-p170-p doi:10.1145/3158133

Why Is Random Testing Effective for Partition Tolerance Bugs?
Rupak Majumdar and Filip Niksic
(MPI-SWS, Germany)

Publisher's Version Article: popl18main-p141-p doi:10.1145/3158134

On Automatically Proving the Correctness of math.h Implementations
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India)

Publisher's Version Article: popl18main-p43-p doi:10.1145/3158135

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)

Publisher's Version Artifacts Functional Article: popl18main-p124-p doi:10.1145/3158136

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)

Publisher's Version Article: popl18main-p31-p doi:10.1145/3158137

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)

Publisher's Version Artifacts Functional Article: popl18main-p276-p doi:10.1145/3158138

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)

Publisher's Version Artifacts Functional Article: popl18main-p197-p doi:10.1145/3158139

Collapsing Towers of Interpreters
Nada Amin and Tiark Rompf
(University of Cambridge, UK; Purdue University, USA)

Publisher's Version Artifacts Functional Article: popl18main-p33-p doi:10.1145/3158140

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)

Publisher's Version Artifacts Functional Article: popl18main-p1-p doi:10.1145/3158141

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)

Publisher's Version Artifacts Functional Article: popl18main-p201-p doi:10.1145/3158142

A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)

Publisher's Version Artifacts Functional Article: popl18main-p251-p doi:10.1145/3158143

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)

Publisher's Version Article: popl18main-p19-p doi:10.1145/3158144

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)

Publisher's Version Artifacts Functional Article: popl18main-p106-p doi:10.1145/3158145

Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi and Justin Hsu
(University of Wisconsin-Madison, USA; University College London, UK)

Publisher's Version Article: popl18main-p172-p doi:10.1145/3158146

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)

Publisher's Version Article: popl18main-p165-p doi:10.1145/3158147

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)

Publisher's Version Article: popl18main-p234-p doi:10.1145/3158148

Synthesis

Strategy Synthesis for Linear Arithmetic Games
Azadeh Farzan and Zachary Kincaid
(University of Toronto, Canada; Princeton University, USA)

Publisher's Version Artifacts Functional Article: popl18main-p207-p doi:10.1145/3158149

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)

Publisher's Version Artifacts Functional Article: popl18main-p282-p doi:10.1145/3158150

Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig, and Rishabh Singh
(University of Texas at Austin, USA; Microsoft Research, USA)

Publisher's Version Article: popl18main-p20-p doi:10.1145/3158151

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)

Publisher's Version Artifacts Functional Article: popl18main-p27-p doi:10.1145/3158152

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)

Publisher's Version Artifacts Functional Article: popl18main-p134-p doi:10.1145/3158153

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)

Publisher's Version Artifacts Functional Article: popl18main-p202-p doi:10.1145/3158154

proc time: 0.13