POPL – Journal Issue

Artifacts Functional Article: popl21main-p12-p doi:10.1145/3434284

Verifying Observational Robustness against a C11-Style Memory Model
Roy Margalit and Ori Lahav
(Tel Aviv University, Israel)

Artifacts Functional Article: popl21main-p24-p doi:10.1145/3434285

On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; Nomadic Labs, France; Complutense University of Madrid, Spain)

Artifacts Functional Article: popl21main-p25-p doi:10.1145/3434286

Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)

Artifacts Functional Article: popl21main-p34-p doi:10.1145/3434287

Fully Abstract from Static to Gradual
Koen Jacobs, Amin Timany, and Dominique Devriese
(KU Leuven, Belgium; Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)

Artifacts Functional Article: popl21main-p38-p doi:10.1145/3434288

Deciding Accuracy of Differential Privacy Schemes
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan
(MPI-SP, Germany; University of Missouri, USA; University of Illinois at Urbana-Champaign, USA; University of Illinois at Chicago, USA)

Artifacts Functional Article: popl21main-p41-p doi:10.1145/3434289

A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
Chao-Hong Chen and Amr Sabry
(Indiana University, USA)

Artifacts Functional Article: popl21main-p58-p doi:10.1145/3434290

Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)

Artifacts Functional Article: popl21main-p59-p doi:10.1145/3434291

Probabilistic Programming Semantics for Name Generation
Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman
(McGill University, Canada; University of Oxford, UK)

Publisher's Version Article: popl21main-p70-p doi:10.1145/3434292

Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner
(Carnegie Mellon University, USA; Stockholm University, Sweden)

Artifacts Functional Article: popl21main-p77-p doi:10.1145/3434293

Transfinite Step-Indexing for Termination
Simon Spies, Neel Krishnaswami, and Derek Dreyer
(MPI-SWS, Germany; University of Cambridge, UK)

Publisher's Version Article: popl21main-p86-p doi:10.1145/3434294

Generating Collection Transformations from Proofs
Michael Benedikt and Pierre Pradic
(University of Oxford, UK)

Publisher's Version Article: popl21main-p96-p doi:10.1145/3434295

Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)

Publisher's Version Article: popl21main-p97-p doi:10.1145/3434296

Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida
(University of Novi Sad, Serbia; DTU, Denmark; Aston University, UK; Imperial College London, UK)

Publisher's Version Article: popl21main-p117-p doi:10.1145/3434297

Verifying Correct Usage of Context-Free API Protocols
Kostas Ferles, Jon Stephens, and Isil Dillig
(University of Texas at Austin, USA)

Publisher's Version Article: popl21main-p124-p doi:10.1145/3434298

Provably Space-Efficient Parallel Functional Programming
Jatin Arora, Sam Westrick, and Umut A. Acar
(Carnegie Mellon University, USA)

Artifacts Functional Article: popl21main-p125-p doi:10.1145/3434299

Data Flow Refinement Type Inference
Zvonimir Pavlinovic, Yusen Su, and Thomas Wies
(New York University, USA; Google, USA; University of Waterloo, Canada)

Publisher's Version Article: popl21main-p144-p doi:10.1145/3434300

Simplifying Dependent Reductions in the Polyhedral Model
Cambridge Yang, Eric Atkinson, and Michael Carbin
(Massachusetts Institute of Technology, USA)

Publisher's Version Article: popl21main-p145-p doi:10.1145/3434301

On the Semantic Expressiveness of Recursive Types
Marco Patrignani, Eric Mark Martin, and Dominique Devriese
(Stanford University, USA; CISPA, Germany; Vrije Universiteit Brussel, Belgium)

Publisher's Version Article: popl21main-p147-p doi:10.1145/3434302

Intrinsically Typed Compilation with Nameless Labels
Arjen Rouvoet, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Radboud University Nijmegen, Netherlands)

Artifacts Functional Article: popl21main-p149-p doi:10.1145/3434303

egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)

Artifacts Functional Article: popl21main-p150-p doi:10.1145/3434304

Asynchronous Effects
Danel Ahman and Matija Pretnar
(University of Ljubljana, Slovenia)

Artifacts Functional Article: popl21main-p157-p doi:10.1145/3434305

Modeling and Analyzing Evaluation Cost of CUDA Kernels
Stefan K. Muller and Jan Hoffmann
(Illinois Institute of Technology, USA; Carnegie Mellon University, USA)

Artifacts Functional Article: popl21main-p159-p doi:10.1145/3434306

Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees
Lucas Silver and Steve Zdancewic
(University of Pennsylvania, USA)

Artifacts Functional Article: popl21main-p164-p doi:10.1145/3434307

A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann
(MPI-SP, Germany; Boston University, USA; MPI-SWS, Germany; Carnegie Mellon University, USA)

Publisher's Version Article: popl21main-p174-p doi:10.1145/3434308

Automatic Differentiation in PCF
Damiano Mazza and Michele Pagani
(CNRS, France; University of Paris, France)

Publisher's Version Article: popl21main-p176-p doi:10.1145/3434309

An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jay P. Lim, Mridul Aanjaneya, John Gustafson, and Santosh Nagarakatte
(Rutgers University, USA; National University of Singapore, Singapore)

Artifacts Functional Article: popl21main-p193-p doi:10.1145/3434310

Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)

Artifacts Functional Article: popl21main-p195-p doi:10.1145/3434311

An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Julian Rosemann, Simon Moll, and Sebastian Hack
(Saarland University, Germany; NEC, Germany)

Artifacts Functional Article: popl21main-p206-p doi:10.1145/3434312

Intersection Types and (Positive) Almost-Sure Termination
Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca
(University of Bologna, Italy; University of Paris, France; IRIF, France; CNRS, France; University of Turin, Italy)

Publisher's Version Article: popl21main-p210-p doi:10.1145/3434313

A Separation Logic for Effect Handlers
Paulo Emílio de Vilhena and François Pottier
(Inria, France)

Artifacts Functional Article: popl21main-p211-p doi:10.1145/3434314

The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis
Anders Alnor Mathiasen and Andreas Pavlogiannis
(Aarhus University, Denmark)

Publisher's Version Article: popl21main-p219-p doi:10.1145/3434315

Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch and Ethan Cecchetti
(MPI-SWS, Germany; Cornell University, USA)

Publisher's Version Article: popl21main-p234-p doi:10.1145/3434316

Optimal Prediction of Synchronization-Preserving Races
Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; Aarhus University, Denmark)

Artifacts Functional Article: popl21main-p243-p doi:10.1145/3434317

A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA)

Artifacts Functional Article: popl21main-p250-p doi:10.1145/3434318

Automata and Fixpoints for Asynchronous Hyperproperties
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem
(University of Münster, Germany)

Publisher's Version Article: popl21main-p255-p doi:10.1145/3434319

Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; University College London, UK; ETH Zurich, Switzerland)

Publisher's Version Article: popl21main-p256-p doi:10.1145/3434320

Verified Code Generation for the Polyhedral Model
Nathanaël Courant and Xavier Leroy
(Inria, France; Collège de France, France; PSL University, France)

Publisher's Version Article: popl21main-p269-p doi:10.1145/3434321

Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)

Artifacts Functional Article: popl21main-p288-p doi:10.1145/3434322

Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)

Artifacts Functional Article: popl21main-p307-p doi:10.1145/3434323

PerSeVerE: Persistency Semantics for Verification under Ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; National Research University Higher School of Economics, Russia; JetBrains Research, Russia; Imperial College London, UK)

Artifacts Functional Article: popl21main-p319-p doi:10.1145/3434324

Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)

Publisher's Version Article: popl21main-p328-p doi:10.1145/3434325

A Practical Mode System for Recursive Definitions
Alban Reynaud, Gabriel Scherer, and Jeremy Yallop
(ENS Lyon, France; Inria, France; University of Cambridge, UK)

Artifacts Functional Article: popl21main-p349-p doi:10.1145/3434326

Formally Verified Speculation and Deoptimization in a JIT Compiler
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Northeastern University, USA; Czech Technical University, Czechia)

Artifacts Functional Article: popl21main-p383-p doi:10.1145/3434327

Taming x86-TSO Persistency
Artem Khyzha and Ori Lahav
(Tel Aviv University, Israel)

Publisher's Version Article: popl21main-p384-p doi:10.1145/3434328

Deciding ω-Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell
(Technion, Israel; MPI-SWS, Germany; University of Oxford, UK)

Publisher's Version Article: popl21main-p394-p doi:10.1145/3434329

Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)

Artifacts Functional Article: popl21main-p403-p doi:10.1145/3434330

A Graded Dependent Type System with a Usage-Aware Semantics
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich
(University of Pennsylvania, USA; Augusta University, USA; Tweag I/O, France; Bryn Mawr College, USA)

Artifacts Functional Article: popl21main-p408-p doi:10.1145/3434331

The (In)Efficiency of Interaction
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni
(Inria, France; École Polytechnique, France; University of Bologna, Italy)

Publisher's Version Article: popl21main-p420-p doi:10.1145/3434332

A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)

Publisher's Version Article: popl21main-p451-p doi:10.1145/3434333

Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn
(Northeastern University, USA; University of Maryland, USA; Indiana University, USA)

Artifacts Functional Article: popl21main-p519-p doi:10.1145/3434334

Combining the Top-Down Propagation and Bottom-Up Enumeration for Inductive Program Synthesis
Woosuk Lee
(Hanyang University, South Korea)

Artifacts Functional Article: popl21main-p535-p doi:10.1145/3434335

Intensional Datatype Refinement: With Application to Scalable Verification of Pattern-Match Safety
Eddie Jones and Steven Ramsay
(University of Bristol, UK)

Artifacts Functional Article: popl21main-p556-p doi:10.1145/3434336

Deciding Reachability under Persistent x86-TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; University of Paris, France; Chennai Mathematical Institute, India; CNRS UMI ReLaX, India; Institute of Mathematical Sciences, India)

Publisher's Version Article: popl21main-p602-p doi:10.1145/3434337

Functorial Semantics for Partial Theories
Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński
(Czech Academy of Sciences, Czechia; Tallinn University of Technology, Estonia)

Publisher's Version Article: popl21main-p649-p doi:10.1145/3434338

Paradoxes of Probabilistic Programming: And How to Condition on Events of Measure Zero with Infinitesimal Probabilities
Jules Jacobs
(Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)

Artifacts Functional Article: popl21main-p660-p doi:10.1145/3434339

On the Complexity of Bidirected Interleaved Dyck-Reachability
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)

Publisher's Version Article: popl21main-p661-p doi:10.1145/3434340

The Taming of the Rew: A Type Theory with Computational Assumptions
Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter
(Delft University of Technology, Netherlands; Inria, France; LS2N, France)