POPL – Journal Issue

Artifacts Reusable Article: popl24main-p107-p doi:10.1145/3632865

The Essence of Generalized Algebraic Data Types
Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, and Lars Birkedal
(Heriot-Watt University, UK; Aarhus University, Denmark; University of Cambridge, UK)

Artifacts Reusable Article: popl24main-p110-p doi:10.1145/3632866

Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
John Cyphert and Zachary Kincaid
(University of Wisconsin-Madison, USA; Princeton University, USA)

Artifacts Reusable Article: popl24main-p122-p doi:10.1145/3632867

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

Info

Artifacts Reusable Article: popl24main-p129-p doi:10.1145/3632868

Quotient Haskell: Lightweight Quotient Types for All
Brandon Hewer and Graham Hutton
(University of Nottingham, UK)

Publisher's Version Article: popl24main-p136-p doi:10.1145/3632869

Semantic Code Refactoring for Abstract Data Types
Shankara Pailoor, Yuepeng Wang, and Işıl Dillig
(University of Texas, Austin, USA; Simon Fraser University, Canada)

Publisher's Version Article: popl24main-p145-p doi:10.1145/3632870

EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
Pu Sun, Fu Song, Yuqi Chen, and Taolue Chen
(ShanghaiTech University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Birkbeck University of London, UK)

Info Article: popl24main-p146-p doi:10.1145/3632871

Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
Julian Müllner, Marcel Moosbrugger, and Laura Kovács
(TU Wien, Austria)

Publisher's Version Article: popl24main-p151-p doi:10.1145/3632872

Coarser Equivalences for Causal Concurrency
Azadeh Farzan and Umang Mathur
(University of Toronto, Canada; National University of Singapore, Singapore)

Publisher's Version Article: popl24main-p160-p doi:10.1145/3632873

Implementation and Synthesis of Math Library Functions
Ian Briggs, Yash Lad, and Pavel Panchekha
(University of Utah, USA)

Publisher's Version Article: popl24main-p164-p doi:10.1145/3632874

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Neta Elad, Oded Padon, and Sharon Shoham
(Tel Aviv University, Israel; VMware Research, USA)

Artifacts Reusable Article: popl24main-p166-p doi:10.1145/3632875

On Learning Polynomial Recursive Programs
Alex Buna-Marginean, Vincent Cheval, Mahsa Shirmohammadi, and James Worrell
(University of Oxford, UK; CNRS - IRIF - Université Paris Cité, France)

Publisher's Version Article: popl24main-p168-p doi:10.1145/3632876

Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh
(Columbia University, USA)

Artifacts Reusable Article: popl24main-p170-p doi:10.1145/3632877

Efficient CHAD
Tom J. Smeding and Matthijs I. L. Vákár
(Utrecht University, Netherlands)

Artifacts Reusable Article: popl24main-p178-p doi:10.1145/3632878

Positive Almost-Sure Termination: Complexity and Proof Rules
Rupak Majumdar and V. R. Sathiyanarayana
(MPI-SWS, Germany)

Publisher's Version Article: popl24main-p180-p doi:10.1145/3632879

Automatic Parallelism Management
Sam Westrick, Matthew Fluet, Mike Rainey, and Umut A. Acar
(Carnegie Mellon University, USA; Rochester Institute of Technology, USA)

Publisher's Version Article: popl24main-p181-p doi:10.1145/3632880

Orthologic with Axioms
Simon Guilloud and Viktor Kunčak
(EPFL, Switzerland)

Publisher's Version Article: popl24main-p183-p doi:10.1145/3632881

Polymorphic Type Inference for Dynamic Languages
Giuseppe Castagna, Mickaël Laurent, and Kim Nguyễn
(CNRS - Université Paris Cité, France; Université Paris Cité, France; Université Paris-Saclay, France)

Archive submitted (1.1 MB)

Artifacts Reusable Article: popl24main-p201-p doi:10.1145/3632882

Fusing Direct Manipulations into Functional Programs
Xing Zhang, Ruifeng Xie, Guanchen Guo, Xiao He, Tao Zan, and Zhenjiang Hu
(Peking University, China; University of Science and Technology Beijing, China; Longyan University, China)

Video

Artifacts Reusable Article: popl24main-p213-p doi:10.1145/3632883

On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
Shankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis, and Omkar Tuppe
(IIT Bombay, India; Aarhus University, Denmark)

Artifacts Reusable Article: popl24main-p214-p doi:10.1145/3632884

Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers
Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi
(IMT School for Advanced Studies Lucca, Italy; University of Pisa, Italy)

Publisher's Version Article: popl24main-p216-p doi:10.1145/3632885

Internalizing Indistinguishability with Dependent Types
Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich
(University of Pennsylvania, USA)

Artifacts Reusable Article: popl24main-p229-p doi:10.1145/3632886

Polyregular Functions on Unordered Trees of Bounded Height
Mikołaj Bojańczyk and Bartek Klin
(University of Warsaw, Poland; University of Oxford, UK)

Publisher's Version Article: popl24main-p231-p doi:10.1145/3632887

The Complex(ity) Landscape of Checking Infinite Descent
Liron Cohen, Adham Jabarin, Andrei Popescu, and Reuben N. S. Rowe
(Ben-Gurion University of the Negev, Israel; University of Sheffield, UK; Royal Holloway University of London, UK)

Archive submitted (300 kB)

Artifacts Reusable Article: popl24main-p233-p doi:10.1145/3632888

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Aarhus University, Denmark)

Artifacts Reusable Article: popl24main-p234-p doi:10.1145/3632889

When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Lionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, and Chun Yin Chau
(Hong Kong University of Science and Technology, Hong Kong; EPFL, Switzerland)

Artifacts Reusable Article: popl24main-p237-p doi:10.1145/3632890

Validation of Modern JSON Schema: Formalization and Complexity
Lyes Attouche, Mohamed-Amine Baazizi, Dario Colazzo, Giorgio Ghelli, Carlo Sartiani, and Stefanie Scherzinger
(Université Paris-Dauphine - PSL, France; Sorbonne University, France; University of Pisa, Italy; University of Basilicata, Italy; University of Passau, Germany)

Artifacts Functional Article: popl24main-p241-p doi:10.1145/3632891

Thunks and Debits in Separation Logic with Time Credits
François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, and Glen Mével
(Inria, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - LMF, France)

Info

Artifacts Reusable Article: popl24main-p245-p doi:10.1145/3632892

Unboxed Data Constructors: Or, How cpp Decides a Halting Problem
Nicolas Chataing, Stephen Dolan, Gabriel Scherer, and Jeremy Yallop
(ENS Paris, France; Jane Street, UK; Inria, France; University of Cambridge, UK)

Publisher's Version Article: popl24main-p252-p doi:10.1145/3632893

Efficient Bottom-Up Synthesis for Programs with Local Variables
Xiang Li, Xiangyu Zhou, Rui Dong, Yihong Zhang, and Xinyu Wang
(University of Michigan, USA; University of Washington, USA)

Artifacts Reusable Article: popl24main-p254-p doi:10.1145/3632894

Disentanglement with Futures, State, and Interaction
Jatin Arora, Stefan K. Muller, and Umut A. Acar
(Carnegie Mellon University, USA; Illinois Institute of Technology, USA)

Publisher's Version Article: popl24main-p260-p doi:10.1145/3632895

Soundly Handling Linearity
Wenhao Tang, Daniel Hillerström, Sam Lindley, and J. Garrett Morris
(University of Edinburgh, UK; Huawei Zurich Research Center, Switzerland; University of Iowa, USA)

Archive submitted (1.5 MB)

Artifacts Reusable Article: popl24main-p261-p doi:10.1145/3632896

Monotonicity and the Precision of Program Analysis
Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, and Caterina Urban
(Inria - ENS - Université PSL, Paris, France; University of Verona, Italy; University of Arizona, Tucson, USA)

Publisher's Version Article: popl24main-p262-p doi:10.1145/3632897

Algebraic Effects Meet Hoare Logic in Cubical Agda
Donnacha Oisín Kidney, Zhixuan Yang, and Nicolas Wu
(Imperial College London, UK)

Artifacts Reusable Article: popl24main-p271-p doi:10.1145/3632898

Solving Infinite-State Games via Acceleration
Philippe Heim and Rayna Dimitrova
(CISPA Helmholtz Center for Information Security, Germany)

Artifacts Reusable Article: popl24main-p273-p doi:10.1145/3632899

Guided Equality Saturation
Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, and Michel Steuwer
(Inria, France; ICube lab - Université de Strasbourg - CNRS, France; University of Amsterdam, Netherlands; University of Edinburgh, UK; University of Cambridge, UK; University of Glasgow, UK; TU Berlin, Germany)

Archive submitted (150 kB) Article: popl24main-p274-p doi:10.1145/3632900

A Case for Synthesis of Recursive Quantum Unitary Programs
Haowei Deng, Runzhou Tao, Yuxiang Peng, and Xiaodi Wu
(University of Maryland, College Park, USA; Columbia University, USA; University of Maryland, USA)

Artifacts Reusable Article: popl24main-p282-p doi:10.1145/3632901

A Formalization of Core Why3 in Coq
Joshua M. Cohen and Philip Johnson-Freyd
(Princeton University, USA; Sandia National Laboratories, USA)

Artifacts Reusable Article: popl24main-p283-p doi:10.1145/3632902

Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
Nate Ackerman, Cameron E. Freer, Younesse Kaddar, Jacek Karwowski, Sean Moss, Daniel Roy, Sam Staton, and Hongseok Yang
(Harvard University, USA; Massachusetts Institute of Technology, USA; University of Oxford, UK; University of Birmingham, UK; University of Toronto, Canada; KAIST, South Korea)

Publisher's Version Article: popl24main-p293-p doi:10.1145/3632903

API-Driven Program Synthesis for Testing Static Typing Implementations
Thodoris Sotiropoulos, Stefanos Chaliasos, and Zhendong Su
(ETH Zurich, Switzerland; Imperial College London, UK)

Artifacts Reusable Article: popl24main-p302-p doi:10.1145/3632904

Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Francesca Randone, Luca Bortolussi, Emilio Incerto, and Mirco Tribastone
(IMT School for Advanced Studies Lucca, Italy; University of Trieste, Italy)

Artifacts Reusable Article: popl24main-p312-p doi:10.1145/3632905

Decision and Complexity of Dolev-Yao Hyperproperties
Itsaka Rakotonirina, Gilles Barthe, and Clara Schneidewind
(MPI-SP, Germany; IMDEA Software Institute, Spain)

Publisher's Version Article: popl24main-p331-p doi:10.1145/3632906

Parikh’s Theorem Made Symbolic
Matthew Hague, Artur Jeż, and Anthony W. Lin
(Royal Holloway University of London, UK; University of Wrocław, Poland; University of Kaiserslautern-Landau, Germany; MPI-SWS, Germany)

Artifacts Functional Article: popl24main-p332-p doi:10.1145/3632907

How Hard Is Weak-Memory Testing?
Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, and Andreas Pavlogiannis
(TU Delft, Netherlands; IIT Bombay, India; National University of Singapore, Singapore; Aarhus University, Denmark)

Publisher's Version Article: popl24main-p333-p doi:10.1145/3632908

Ill-Typed Programs Don’t Evaluate
Steven Ramsay and Charlie Walpole
(University of Bristol, UK)

Publisher's Version Article: popl24main-p334-p doi:10.1145/3632909

Total Type Error Localization and Recovery with Holes
Eric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, and Cyrus Omar
(University of Michigan, USA)

Artifacts Reusable Article: popl24main-p336-p doi:10.1145/3632910

VST-A: A Foundationally Sound Annotation Verifier
Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, and Qinxiang Cao
(Shanghai Jiao Tong University, China; University of Hong Kong, China; Princeton University, USA)

Artifacts Reusable Article: popl24main-p348-p doi:10.1145/3632911

Mechanizing Refinement Types
Michael H. Borkowski, Niki Vazou, and Ranjit Jhala
(University of California, San Diego, USA; IMDEA Software Institute, Spain)

Artifacts Reusable Article: popl24main-p349-p doi:10.1145/3632912

Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
Yuantian Ding and Xiaokang Qiu
(Purdue University, USA)

Artifacts Reusable Article: popl24main-p375-p doi:10.1145/3632913

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, and Zhong Shao
(Shanghai Jiao Tong University, China; Yale University, USA)

Artifacts Reusable Article: popl24main-p380-p doi:10.1145/3632914

Predictive Monitoring against Pattern Regular Languages
Zhendong Ang and Umang Mathur
(National University of Singapore, Singapore)

Artifacts Reusable Article: popl24main-p382-p doi:10.1145/3632915

Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Ștefan Ciobâcă, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, and Théo Winterhalter
(MPI-SP, Germany; Alexandru Ioan Cuza University, Iași, Romania; Microsoft Research, USA; Tallinn University of Technology, Estonia; University of Chile, Chile; Inria, France)

Artifacts Reusable Article: popl24main-p385-p doi:10.1145/3632916

ReLU Hull Approximation
Zhongkui Ma, Jiaying Li, and Guangdong Bai
(University of Queensland, Australia; Microsoft, China)

Publisher's Version Article: popl24main-p441-p doi:10.1145/3632917

Polynomial Time and Dependent Types
Robert Atkey
(University of Strathclyde, UK)

Artifacts Functional Article: popl24main-p453-p doi:10.1145/3632918

Generating Well-Typed Terms That Are Not “Useless”
Justin Frank, Benjamin Quiring, and Leonidas Lampropoulos
(University of Maryland, College Park, USA)

Artifacts Reusable Article: popl24main-p476-p doi:10.1145/3632919

Internal Parametricity, without an Interval
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman
(University of Nottingham, UK; École Polytechnique, France; Eötvös Loránd University, Hungary; University of San Diego, USA)

Publisher's Version Article: popl24main-p508-p doi:10.1145/3632920

Explicit Effects and Effect Constraints in ReML
Martin Elsman
(University of Copenhagen, Denmark)

Artifacts Reusable Article: popl24main-p536-p doi:10.1145/3632921

Indexed Types for a Statically Safe WebAssembly
Adam T. Geller, Justin Frank, and William J. Bowman
(University of British Columbia, Canada; University of Maryland, USA)

Artifacts Functional Article: popl24main-p538-p doi:10.1145/3632922

SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
Yuxiang Peng, Jacob Young, Pengyu Liu, and Xiaodi Wu
(University of Maryland, USA; Carnegie Mellon University, USA)

Info

Artifacts Reusable Article: popl24main-p544-p doi:10.1145/3632923

A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, and Lizzie Hernandez
(Dartmouth College, USA; Google Research, USA; Boston University, USA; Microsoft, USA)

Artifacts Reusable Article: popl24main-p557-p doi:10.1145/3632924

Commutativity Simplifies Proofs of Parameterized Programs
Azadeh Farzan, Dominik Klumpp, and Andreas Podelski
(University of Toronto, Canada; University of Freiburg, Germany)

Artifacts Available Article: popl24main-p579-p doi:10.1145/3632925

Higher Order Bayesian Networks, Exactly
Claudia Faggian, Daniele Pautasso, and Gabriele Vanoni
(IRIF - CNRS - Université Paris Cité, France; University of Turin, Italy)

Publisher's Version Article: popl24main-p582-p doi:10.1145/3632926

Sound Gradual Verification with Symbolic Execution
Conrad Zimmerman, Jenna DiVincenzo, and Jonathan Aldrich
(Brown University, USA; Purdue University, USA; Carnegie Mellon University, USA)

Info Article: popl24main-p589-p doi:10.1145/3632927

Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
Supun Abeysinghe, Anxhelo Xhebraj, and Tiark Rompf
(Purdue University, USA)

Publisher's Version Article: popl24main-p634-p doi:10.1145/3632928

On Model-Checking Higher-Order Effectful Programs
Ugo Dal Lago and Alexis Ghyselen
(University of Bologna, Italy)

Publisher's Version Article: popl24main-p635-p doi:10.1145/3632929

Effectful Software Contracts
Cameron Moy, Christos Dimoulas, and Matthias Felleisen
(PLT at Northeastern University, USA; PLT at Northwestern University, USA)

Artifacts Reusable Article: popl24main-p642-p doi:10.1145/3632930

Type-Based Gradual Typing Performance Optimization
John Peter Campora, Mohammad Wahiduzzaman Khan, and Sheng Chen
(Quantinuum, USA; University of Louisiana, Lafayette, USA)

Publisher's Version Article: popl24main-p713-p doi:10.1145/3632931

Parametric Subtyping for Structural Parametric Polymorphism
Henry DeYoung, Andreia Mordido, Frank Pfenning, and Ankush Das
(Carnegie Mellon University, USA; Universidade de Lisboa, Portugal; Amazon, USA)

Info

Artifacts Reusable Article: popl24main-p714-p doi:10.1145/3632932

Inference of Robust Reachability Constraints
Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, and Sébastien Bardin
(Université Grenoble-Alpes - CEA - List, France; Université Paris-Saclay - CEA - List, France)