


default search action
Proceedings of the ACM on Programming Languages, Volume 8
Volume 8, Number POPL, January 2024
- Pascal Bergsträßer
, Moses Ganardi
, Anthony W. Lin
, Georg Zetzsche
:
Ramsey Quantifiers in Linear Arithmetics. 1-32 - Jens Oliver Gutsfeld
, Markus Müller-Olm
, Christoph Ohrem
:
Deciding Asynchronous Hyperproperties for Recursive Programs. 33-60 - Xueying Qin
, Liam O'Connor
, Rob van Glabbeek
, Peter Höfner
, Ohad Kammar
, Michel Steuwer
:
Shoggoth: A Formal Foundation for Strategic Rewriting. 61-89 - A. R. Balasubramanian
, Rupak Majumdar
, Ramanathan S. Thinniyam
, Georg Zetzsche
:
Reachability in Continuous Pushdown VASS. 90-114 - Fuga Kawamata
, Hiroshi Unno
, Taro Sekiyama
, Tachio Terauchi
:
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. 115-147 - William Mansky
, Ke Du
:
An Iris Instance for Verifying CompCert C Programs. 148-174 - Patrick Cousot
:
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation. 175-208 - Antoine Van Muylder
, Andreas Nuyts
, Dominique Devriese
:
Internal and Observational Parametricity for Cubical Agda. 209-240 - Amin Timany
, Simon Oddershede Gregersen
, Léo Stefanesco
, Jonas Kastberg Hinrichsen
, Léon Gondelman
, Abel Nieto
, Lars Birkedal
:
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. 241-272 - Harrison Grodin
, Yue Niu
, Jonathan Sterling
, Robert Harper
:
Decalf: A Directed, Effectful Cost-Aware Logical Framework. 273-301 - Alexandre Moine
, Sam Westrick
, Stephanie Balzer
:
DisLog: A Separation Logic for Disentanglement. 302-331 - Dan Frumin
, Amin Timany
, Lars Birkedal
:
Modular Denotational Semantics for Effects with Guarded Interaction Trees. 332-361 - Takeshi Tsukada
, Kazuyuki Asada
:
Enriched Presheaf Model of Quantum FPC. 362-392 - Guannan Wei
, Oliver Bracevac
, Songlin Jia
, Yuyan Bao
, Tiark Rompf
:
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. 393-424 - Andrei Popescu
:
Nominal Recursors as Epi-Recursors. 425-456 - Stephen Mell
, Steve Zdancewic
, Osbert Bastani
:
Optimal Program Synthesis via Abstract Interpretation. 457-481 - Francis Rinaldi
, june wunder
, Arthur Azevedo de Amorim
, Stefan K. Muller
:
Pipelines and Beyond: Graph Types for ADTs with Futures. 482-511 - Noah Patton
, Kia Rahmani
, Meghana Missula
, Joydeep Biswas
, Isil Dillig
:
Programming-by-Demonstration for Long-Horizon Robot Tasks. 512-545 - Jacques Carette
, Chris Heunen
, Robin Kaarsgaard
, Amr Sabry
:
With a Few Square Roots, Quantum Computing Is as Easy as Pi. 546-574 - Amin Timany
, Armaël Guéneau
, Lars Birkedal
:
The Logical Essence of Well-Bracketed Control Flow. 575-603 - Angus Hammond
, Zongyuan Liu
, Thibaut Pérami
, Peter Sewell
, Lars Birkedal
, Jean Pichon-Pharabod
:
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. 604-637 - Chih-Duo Hong
, Anthony W. Lin
:
Regular Abstractions for Array Systems. 638-666 - Will Crichton
, Shriram Krishnamurthi
:
A Core Calculus for Documents: Or, Lambda: The Ultimate Document. 667-694 - Filip Sieczkowski
, Sergei Stepanenko
, Jonathan Sterling
, Lars Birkedal
:
The Essence of Generalized Algebraic Data Types. 695-723 - John Cyphert
, Zachary Kincaid
:
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis. 724-752 - Simon Oddershede Gregersen
, Alejandro Aguirre
, Philipp G. Haselwarter
, Joseph Tassarotti
, Lars Birkedal
:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. 753-784 - Brandon Hewer
, Graham Hutton
:
Quotient Haskell: Lightweight Quotient Types for All. 785-815 - Shankara Pailoor
, Yuepeng Wang
, Isil Dillig
:
Semantic Code Refactoring for Abstract Data Types. 816-847 - Pu Sun
, Fu Song
, Yuqi Chen
, Taolue Chen
:
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis. 848-881 - Julian Müllner
, Marcel Moosbrugger
, Laura Kovács
:
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. 882-910 - Azadeh Farzan
, Umang Mathur
:
Coarser Equivalences for Causal Concurrency. 911-941 - Ian Briggs
, Yash Lad
, Pavel Panchekha
:
Implementation and Synthesis of Math Library Functions. 942-969 - Neta Elad
, Oded Padon
, Sharon Shoham
:
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. 970-1000 - Alex Buna-Marginean
, Vincent Cheval
, Mahsa Shirmohammadi
, James Worrell
:
On Learning Polynomial Recursive Programs. 1001-1027 - Jianan Yao
, Runzhou Tao
, Ronghui Gu
, Jason Nieh
:
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions. 1028-1059 - Tom Smeding
, Matthijs Vákár
:
Efficient CHAD. 1060-1088 - Rupak Majumdar
, V. R. Sathiyanarayana
:
Positive Almost-Sure Termination: Complexity and Proof Rules. 1089-1117 - Sam Westrick
, Matthew Fluet
, Mike Rainey
, Umut A. Acar
:
Automatic Parallelism Management. 1118-1149 - Simon Guilloud
, Viktor Kuncak
:
Orthologic with Axioms. 1150-1178 - Giuseppe Castagna
, Mickaël Laurent
, Kim Nguyen
:
Polymorphic Type Inference for Dynamic Languages. 1179-1210 - Xing Zhang
, Ruifeng Xie
, Guanchen Guo
, Xiao He
, Tao Zan
, Zhenjiang Hu
:
Fusing Direct Manipulations into Functional Programs. 1211-1238 - Shankaranarayanan Krishna
, Aniket Lal
, Andreas Pavlogiannis
, Omkar Tuppe
:
On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability. 1239-1268 - Lorenzo Ceragioli
, Fabio Gadducci
, Giuseppe Lomurno
, Gabriele Tedeschi
:
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers. 1269-1297 - Yiyun Liu
, Jonathan Chan
, Jessica Shi
, Stephanie Weirich
:
Internalizing Indistinguishability with Dependent Types. 1298-1325 - Mikolaj Bojanczyk
, Bartek Klin
:
Polyregular Functions on Unordered Trees of Bounded Height. 1326-1351 - Liron Cohen
, Adham Jabarin
, Andrei Popescu
, Reuben N. S. Rowe
:
The Complex(ity) Landscape of Checking Infinite Descent. 1352-1384 - Jules Jacobs
, Jonas Kastberg Hinrichsen
, Robbert Krebbers
:
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. 1385-1417 - Lionel Parreaux
, Aleksander Boruch-Gruszecki
, Andong Fan
, Chun Yin Chau
:
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism. 1418-1450 - Lyes Attouche
, Mohamed-Amine Baazizi
, Dario Colazzo
, Giorgio Ghelli
, Carlo Sartiani
, Stefanie Scherzinger
:
Validation of Modern JSON Schema: Formalization and Complexity. 1451-1481 - François Pottier
, Armaël Guéneau
, Jacques-Henri Jourdan
, Glen Mével
:
Thunks and Debits in Separation Logic with Time Credits. 1482-1508 - Nicolas Chataing
, Stephen Dolan
, Gabriel Scherer
, Jeremy Yallop
:
Unboxed Data Constructors: Or, How cpp Decides a Halting Problem. 1509-1539 - Xiang Li
, Xiangyu Zhou
, Rui Dong
, Yihong Zhang
, Xinyu Wang
:
Efficient Bottom-Up Synthesis for Programs with Local Variables. 1540-1568 - Jatin Arora
, Stefan K. Muller
, Umut A. Acar
:
Disentanglement with Futures, State, and Interaction. 1569-1599 - Wenhao Tang
, Daniel Hillerström
, Sam Lindley
, J. Garrett Morris
:
Soundly Handling Linearity. 1600-1628 - Marco Campion
, Mila Dalla Preda
, Roberto Giacobazzi
, Caterina Urban
:
Monotonicity and the Precision of Program Analysis. 1629-1662 - Donnacha Oisín Kidney
, Zhixuan Yang
, Nicolas Wu
:
Algebraic Effects Meet Hoare Logic in Cubical Agda. 1663-1695 - Philippe Heim
, Rayna Dimitrova
:
Solving Infinite-State Games via Acceleration. 1696-1726 - Thomas Koehler
, Andrés Goens
, Siddharth Bhat
, Tobias Grosser
, Phil Trinder
, Michel Steuwer
:
Guided Equality Saturation. 1727-1758 - Haowei Deng
, Runzhou Tao
, Yuxiang Peng
, Xiaodi Wu
:
A Case for Synthesis of Recursive Quantum Unitary Programs. 1759-1788 - Joshua M. Cohen
, Philip Johnson-Freyd
:
A Formalization of Core Why3 in Coq. 1789-1818 - Nathanael L. Ackerman
, Cameron E. Freer
, Younesse Kaddar
, Jacek Karwowski
, Sean K. Moss
, Daniel M. Roy
, Sam Staton
, Hongseok Yang
:
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets. 1819-1849 - Thodoris Sotiropoulos
, Stefanos Chaliasos
, Zhendong Su
:
API-Driven Program Synthesis for Testing Static Typing Implementations. 1850-1881 - Francesca Randone
, Luca Bortolussi
, Emilio Incerto
, Mirco Tribastone
:
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures. 1882-1912 - Itsaka Rakotonirina
, Gilles Barthe
, Clara Schneidewind
:
Decision and Complexity of Dolev-Yao Hyperproperties. 1913-1944 - Matthew Hague
, Artur Jez
, Anthony W. Lin
:
Parikh's Theorem Made Symbolic. 1945-1977 - Soham Chakraborty
, Shankara Narayanan Krishna
, Umang Mathur
, Andreas Pavlogiannis
:
How Hard Is Weak-Memory Testing? 1978-2009 - Steven Ramsay
, Charlie Walpole
:
Ill-Typed Programs Don't Evaluate. 2010-2040 - Eric Zhao
, Raef Maroof
, Anand Dukkipati
, Andrew Blinn
, Zhiyi Pan
, Cyrus Omar
:
Total Type Error Localization and Recovery with Holes. 2041-2068 - Litao Zhou
, Jianxing Qin
, Qinshi Wang
, Andrew W. Appel
, Qinxiang Cao
:
VST-A: A Foundationally Sound Annotation Verifier. 2069-2098 - Michael Borkowski
, Niki Vazou
, Ranjit Jhala
:
Mechanizing Refinement Types. 2099-2128 - Yuantian Ding
, Xiaokang Qiu
:
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations. 2129-2159 - Ling Zhang
, Yuting Wang
, Jinhua Wu
, Jérémie Koenig
, Zhong Shao
:
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. 2160-2190 - Zhendong Ang
, Umang Mathur
:
Predictive Monitoring against Pattern Regular Languages. 2191-2225 - Cezar-Constantin Andrici
, Stefan Ciobaca
, Catalin Hritcu
, Guido Martínez
, Exequiel Rivas
, Éric Tanter
, Théo Winterhalter
:
Securing Verified IO Programs Against Unverified Code in F. 2226-2259 - Zhongkui Ma
, Jiaying Li
, Guangdong Bai
:
ReLU Hull Approximation. 2260-2287 - Robert Atkey
:
Polynomial Time and Dependent Types. 2288-2317 - Justin Frank
, Benjamin Quiring
, Leonidas Lampropoulos
:
Generating Well-Typed Terms That Are Not "Useless". 2318-2339 - Thorsten Altenkirch
, Yorgo Chamoun
, Ambrus Kaposi
, Michael Shulman
:
Internal Parametricity, without an Interval. 2340-2369 - Martin Elsman
:
Explicit Effects and Effect Constraints in ReML. 2370-2394 - Adam T. Geller
, Justin Frank
, William J. Bowman
:
Indexed Types for a Statically Safe WebAssembly. 2395-2424 - Yuxiang Peng
, Jacob Young
, Pengyu Liu
, Xiaodi Wu
:
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation. 2425-2455 - Prasad Jayanti
, Siddhartha Jayanti
, Ugur Y. Yavuz
, Lizzie Hernandez
:
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability. 2456-2484 - Azadeh Farzan
, Dominik Klumpp
, Andreas Podelski
:
Commutativity Simplifies Proofs of Parameterized Programs. 2485-2513 - Claudia Faggian
, Daniele Pautasso
, Gabriele Vanoni
:
Higher Order Bayesian Networks, Exactly. 2514-2546 - Conrad Zimmerman
, Jenna DiVincenzo
, Jonathan Aldrich
:
Sound Gradual Verification with Symbolic Execution. 2547-2576 - Supun Abeysinghe
, Anxhelo Xhebraj
, Tiark Rompf
:
Flan: An Expressive and Efficient Datalog Compiler for Program Analysis. 2577-2609 - Ugo Dal Lago
, Alexis Ghyselen
:
On Model-Checking Higher-Order Effectful Programs. 2610-2638 - Cameron Moy
, Christos Dimoulas
, Matthias Felleisen
:
Effectful Software Contracts. 2639-2666 - John Peter Campora III
, Mohammad Wahiduzzaman Khan
, Sheng Chen
:
Type-Based Gradual Typing Performance Optimization. 2667-2699 - Henry DeYoung
, Andreia Mordido
, Frank Pfenning
, Ankush Das
:
Parametric Subtyping for Structural Parametric Polymorphism. 2700-2730 - Yanis Sellami
, Guillaume Girol
, Frédéric Recoules
, Damien Couroussé
, Sébastien Bardin
:
Inference of Robust Reachability Constraints. 2731-2760 - Konstantinos Mamouras
, Agnishom Chattopadhyay
:
Efficient Matching of Regular Expressions with Lookaround Assertions. 2761-2791 - Kevin Batz
, Tom Jannik Biskup
, Joost-Pieter Katoen
, Tobias Winkler
:
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. 2792-2820
Volume 8, Number PLDI, 2024
- Debangshu Banerjee
, Changming Xu
, Gagandeep Singh
:
Input-Relational Verification of Deep Neural Networks. 1-27 - Minseong Jang
, Jungin Rhee
, Woojin Lee
, Shuangshuang Zhao
, Jeehoon Kang
:
Modular Hardware Design of Pipelined Circuits with Hazards. 28-51 - Yannick Forster
, Matthieu Sozeau
, Nicolas Tabareau
:
Verified Extraction from Coq to OCaml. 52-75 - Long Pham
, Feras A. Saad
, Jan Hoffmann
:
Robust Resource Bounds with Static Analysis and Bayesian Inference. 76-101 - Qiantan Hong
, Alex Aiken
:
Recursive Program Synthesis using Paramorphisms. 102-125 - Aleksandar Krastev
, Nikola Samardzic
, Simon Langowski
, Srinivas Devadas
, Daniel Sánchez
:
A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption. 126-150 - Jaehwang Jung
, Jeonghyeon Kim
, Matthew J. Parkinson
, Jeehoon Kang
:
Concurrent Immediate Reference Counting. 151-174 - Sunho Park
, Jaewoo Kim
, Ike Mulder
, Jaehwang Jung
, Janggun Lee
, Robbert Krebbers
, Jeehoon Kang
:
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. 175-198 - Siva Kesava Reddy Kakarla
, Francis Y. Yan
, Ryan Beckett
:
Diffy: Data-Driven Bug Finding for Configurations. 199-222 - Shaohua Li
, Theodoros Theodoridis
, Zhendong Su
:
Boosting Compiler Testing by Injecting Real-World Code. 223-245 - Benjamin Mikek
, Qirun Zhang
:
SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories. 246-271 - Ritvik Sharma
, Sara Achour
:
Compilation of Qubit Circuits to Optimized Qutrit Circuits. 272-295 - Aditya Anand
, Solai Adithya
, Swapnil Rustagi
, Priyam Seth
, Vijay Sundaresan
, Daryl Maier
, V. Krishna Nandivada
, Manas Thakur
:
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes. 296-319 - Amanda Liu
, Gilbert Bernstein
, Adam Chlipala
, Jonathan Ragan-Kelley
:
A Verified Compiler for a Functional Tensor Language. 320-342 - Chujun Geng
, Spyros Blanas
, Michael D. Bond
, Yang Wang
:
IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications. 343-367 - Dorian Lesbre
, Matthieu Lemerre
:
Compiling with Abstract Interpretation. 368-393 - Matthew Lutze
, Magnus Madsen
:
Associated Effects: Flexible Abstractions for Effectful Programming. 394-416 - Mafalda Ferreira
, Miguel Monteiro
, Tiago Brito
, Miguel E. Coimbra
, Nuno Santos
, Limin Jia
, José Fragoso Santos
:
Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs. 417-441 - Joao Rivera
, Franz Franchetti
, Markus Püschel
:
Floating-Point TVPI Abstract Domain. 442-466 - Ajay Brahmakshatriya
, Martin C. Rinard, Manya Ghobadi
, Saman P. Amarasinghe
:
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks. 467-491 - Charles Yuan
, Michael Carbin
:
The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation. 492-517 - Anton Lorenzen
, Daan Leijen
, Wouter Swierstra
, Sam Lindley
:
The Functional Essence of Imperative Binary Search Trees. 518-542 - Mikhail Svyatlovskiy
, Shai Mermelstein
, Ori Lahav
:
Compositional Semantics for Shared-Variable Concurrency. 543-566 - Peisen Yao
, Jinguo Zhou
, Xiao Xiao
, Qingkai Shi
, Rongxin Wu
, Charles Zhang
:
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis. 567-592 - Hongzheng Chen
, Niansong Zhang
, Shaojie Xiang
, Zhichen Zeng
, Mengjia Dai
, Zhiru Zhang
:
Allo: A Programming Model for Composable Accelerator Design. 593-620