![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
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 - Joseph Raskind
, Timur Babakol
, Khaled Mahmoud
, Yu David Liu
:
VESTA: Power Modeling with Language Runtime Events. 621-646 - Vladimir Gladshtein
, Qiyuan Zhao
, Willow Ahrens
, Saman P. Amarasinghe
, Ilya Sergey
:
Mechanised Hypersafety Proofs about Structured Data. 647-670 - Theodoros Theodoridis
, Zhendong Su
:
Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior. 671-691 - Thomas Ball
, Peli de Halleux
, James Devine
, Steve Hodges
, Michal Moskal
:
Jacdac: Service-Based Prototyping of Embedded Systems. 692-715 - Jaemin Hong
, Sukyoung Ryu
:
Don't Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation. 716-740 - Guillaume Girol
, Guilhem Lacombe
, Sébastien Bardin
:
Quantitative Robustness for Vulnerability Assessment. 741-765 - George Zakhour
, Pascal Weisenburger
, Guido Salvaneschi
:
Automated Verification of Fundamental Algebraic Laws. 766-789 - Mathieu Huot
, Matin Ghavami
, Alexander K. Lew
, Ulrich Schaechtle
, Cameron E. Freer
, Zane Shelby
, Martin C. Rinard
, Feras A. Saad
, Vikash K. Mansinghka
:
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables. 790-815 - Iavor S. Diatchki
, Mike Dodds
, Harrison Goldstein
, Bill Harris
, David A. Holland
, Benoît Razet
, Cole Schlesinger
, Simon Winwood
:
Daedalus: Safer Document Parsing. 816-840 - Bastian Köpcke
, Sergei Gorlatch
, Michel Steuwer
:
Descend: A Safe GPU Systems Programming Language. 841-864 - Poorva Garg
, Steven Holtzen
, Guy Van den Broeck
, Todd D. Millstein
:
Bit Blasting Probabilistic Programs. 865-888 - Simon Spies
, Lennard Gäher
, Michael Sammler
, Derek Dreyer
:
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. 889-913 - Jiawen Liu
, Weihao Qu
, Marco Gaboardi
, Deepak Garg
, Jonathan R. Ullman
:
Program Analysis for Adaptive Data Analysis. 914-938 - Ruyi Ji
, Yuwei Zhao
, Nadia Polikarpova
, Yingfei Xiong
, Zhenjiang Hu
:
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. 939-964 - Guannan Wei
, Danning Xie
, Wuqi Zhang
, Yongwei Yuan
, Zhuo Zhang
:
Consolidating Smart Contracts with Behavioral Contracts. 965-989 - Christian Wimmer
, Codrut Stancu
, David Kozak
, Thomas Würthinger
:
Scaling Type-Based Points-to Analysis with Saturation. 990-1013 - Ziteng Wang
, Shankara Pailoor
, Aaryan Prakash
, Yuepeng Wang
, Isil Dillig
:
From Batch to Stream: Automatic Generation of Online Algorithms. 1014-1039 - Wang Fang
, Mingsheng Ying
:
Symbolic Execution for Quantum Error Correction Programs. 1040-1065 - Blake Pelton
, Adam Sapek
, Ken Eguro
, Daniel Lo
, Alessandro Forin
, Matt Humphrey
, Jinwen Xi
, David Cox
, Rajas Karandikar
, Johannes de Fine Licht
, Evgeny Babin
, Adrian M. Caulfield
, Doug Burger
:
Wavefront Threading Enables Effective High-Level Synthesis. 1066-1090 - Julia Belyakova
, Benjamin Chung
, Ross Tate
, Jan Vitek
:
Decidable Subtyping of Existential Types for Julia. 1091-1114 - Lennard Gäher
, Michael Sammler
, Ralf Jung
, Robbert Krebbers
, Derek Dreyer
:
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. 1115-1139 - Longfei Qiu
, Yoonseung Kim
, Ji-Yong Shin
, Jieung Kim
, Wolf Honoré
, Zhong Shao
:
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. 1140-1164 - Mathias Rud Laursen
, Wenyuan Xu
, Anders Møller
:
Reducing Static Analysis Unsoundness with Approximate Interpretation. 1165-1188 - Parosh Aziz Abdulla
, Mohamed Faouzi Atig
, Ahmed Bouajjani
, K. Narayan Kumar
, Prakash Saivasan
:
Verification under Intel-x86 with Persistency. 1189-1212 - Genghan Zhang
, Olivia Hsu
, Fredrik Kjolstad
:
Compilation of Modular and General Sparse Workspaces. 1213-1238 - Mridul Aanjaneya
, Santosh Nagarakatte
:
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation. 1239-1263 - Hanru Jiang
:
Qubit Recycling Revisited. 1264-1287 - Ameya Ketkar
, Daniel Ramos
, Lazaro Clapp
, Raj Barik
, Murali Krishna Ramanathan
:
A Lightweight Polyglot Code Transformation Language. 1288-1312 - Anita Buckley
, Pavel Chuprikov
, Rodrigo Otoni
, Robert Soulé
, Robert Rand
, Patrick Eugster
:
An Algebraic Language for Specifying Quantum Networks. 1313-1335 - Aurèle Barrière
, Clément Pit-Claudel
:
Linear Matching of JavaScript Regular Expressions. 1336-1360 - Peixin Wang
, Tengshun Yang
, Hongfei Fu
, Guanyan Li
, C.-H. Luke Ong
:
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. 1361-1386 - Zhe Zhou
, Qianchuan Ye
, Benjamin Delaware
, Suresh Jagannathan
:
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata. 1387-1411 - Joseph W. Cutler
, Christopher Watson
, Emeka Nkurumeh
, Phillip Hilliard
, Harrison Goldstein
, Caleb Stanford
, Benjamin C. Pierce
:
Stream Types. 1412-1436 - Elvira Albert
, Maria Garcia de la Banda
, Alejandro Hernández-Cerezo
, Alexey Ignatiev
, Albert Rubio
, Peter J. Stuckey
:
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. 1437-1462 - Keli Huang
, Jens Palsberg
:
Compiling Conditional Quantum Gates without Using Helper Qubits. 1463-1484 - Thibault Dardinier
, Peter Müller
:
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. 1485-1509 - Gaurav Parthasarathy
, Thibault Dardinier
, Benjamin Bonneau
, Peter Müller
, Alexander J. Summers
:
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. 1510-1534 - Samuel Gruetter
, Viktor Fukala
, Adam Chlipala
:
Live Verification in an Interactive Proof Assistant. 1535-1558 - Dongjun Youn
, Wonho Shin
, Jaehyun Lee
, Sukyoung Ryu
, Joachim Breitner
, Philippa Gardner
, Sam Lindley
, Matija Pretnar
, Xiaojia Rao
, Conrad Watt
, Andreas Rossberg
:
Bringing the WebAssembly Standard up to Speed with SpecTec. 1559-1584 - Atsushi Igarashi
, Shota Ozaki
, Taro Sekiyama
, Yudai Tanabe
:
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric. 1585-1608 - Tianyu Chen
, Jeremy G. Siek
:
Quest Complete: The Holy Grail of Gradual Security. 1609-1632 - Qiuping Yi
, Yifan Yu
, Guowei Yang
:
Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding. 1633-1655 - Michael Fitzgibbons
, Zoe Paraskevopoulou
, Noble Mushtak
, Michelle Thalakottur
, Jose Sulaiman Manzur
, Amal Ahmed
:
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. 1656-1679 - Avery Laird
, Bangtian Liu
, Nikolaj Bjørner
, Maryam Mehri Dehnavi
:
SpEQ: Translation of Sparse Codes using Equivalences. 1680-1703 - Andres Erbsen
, Jade Philipoom
, Dustin Jamner
, Ashley Lin
, Samuel Gruetter
, Clément Pit-Claudel
, Adam Chlipala
:
Foundational Integration Verification of a Cryptographic Server. 1704-1729 - Guofeng Cui
, Yuning Wang
, Wenjie Qiu
, He Zhu
:
Reward-Guided Synthesis of Intelligent Agents with Control Structures. 1730-1754 - Jianlin Li
, Eric Wang
, Yizhou Zhang
:
Compiling Probabilistic Programs for Variable Elimination with Information Flow. 1755-1780 - Michalis Kokologiannakis
, Iason Marmanis
, Viktor Vafeiadis
:
SPORE: Combining Symmetry and Partial Order Reduction. 1781-1803 - Adithya Murali
, Cody Rivera
, P. Madhusudan
:
Predictable Verification using Intrinsic Definitions. 1804-1829 - Yuxiang Lei
, Camille Bossut
, Yulei Sui
, Qirun Zhang
:
Context-Free Language Reachability via Skewed Tabulation. 1830-1853 - Arjun Pitchanathan
, Kunwar Grover
, Tobias Grosser
:
Falcon: A Scalable Analytical Cache Model. 1854-1878 - Justin Lubin
, Jeremy Ferguson
, Kevin Ye
, Jacob Yim
, Sarah E. Chasins
:
Equivalence by Canonicalization for Synthesis-Backed Refactoring. 1879-1904 - Mark Moeller
, Jules Jacobs
, Olivier Savary Bélanger
, David Darais
, Cole Schlesinger
, Steffen Smolka
, Nate Foster
, Alexandra Silva
:
KATch: A Fast Symbolic Verifier for NetKAT. 1905-1928 - Yann Herklotz
, John Wickerson
:
Hyperblock Scheduling for Verified High-Level Synthesis. 1929-1953 - Ariel E. Kellison
, Justin Hsu
:
Numerical Fuzz: A Type System for Rounding Error Analysis. 1954-1978 - Takeshi Tsukada
, Hiroshi Unno
:
Inductive Approach to Spacer. 1979-2002 - Xiaodong Jia
, Gang Tan
:
V-Star: Learning Visibly Pushdown Grammars from Program Inputs. 2003-2026 - Lasse Blaauwbroek
, Miroslav Olsák
, Herman Geuvers
:
Hashing Modulo Context-Sensitive 𝛼-Equivalence. 2027-2050 - Gabriel Matute
, Wode Ni
, Titus Barik
, Alvin Cheung
, Sarah E. Chasins
:
Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments. 2051-2072 - Konstantinos Mamouras
, Alexis Le Glaunec
, Wu Angela Li
, Agnishom Chattopadhyay
:
Static Analysis for Checking the Disambiguation Robustness of Regular Expressions. 2073-2097 - Krishnendu Chatterjee
, Ehsan Kafshdar Goharshady
, Petr Novotný
, Dorde Zikelic:
Equivalence and Similarity Refutation for Probabilistic Programs. 2098-2122 - McCoy R. Becker
, Alexander K. Lew
, Xiaoyan Wang
, Matin Ghavami
, Mathieu Huot
, Martin C. Rinard
, Vikash K. Mansinghka
:
Probabilistic Programming with Programmable Variational Inference. 2123-2147 - Minseok Jeon
, Jihyeok Park
, Hakjoo Oh
:
PL4XGL: A Programming Language Approach to Explainable Graph Learning. 2148-2173 - Ruslan Nikolaev
, Binoy Ravindran
:
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation. 2174-2198
Volume 8, Number OOPSLA1, 2024
- Charles Yuan
, Agnes Villanyi, Michael Carbin:
Quantum Control Machine: The Limits of Control Flow in Quantum Programming. 1-28 - Will Crichton
, Shriram Krishnamurthi
:
Profiling Programming Language Learning. 29-54 - Anouk Paradis, Jasper Dekoninck, Benjamin Bichsel
, Martin T. Vechev:
Synthetiq: Fast and Versatile Quantum Circuit Synthesis. 55-82 - Aashish Yadavally
, Yi Li, Shaohua Wang, Tien N. Nguyen:
A Learning-Based Approach to Static Program Slicing. 83-109 - Chi Zhang
, Linzhang Wang
, Manuel Rigger:
Finding Cross-Rule Optimization Bugs in Datalog Engines. 110-136 - Jie Liu, Zhongyuan Zhao
, Zijian Ding
, Benjamin Brock
, Hongbo Rong
, Zhiru Zhang
:
UniSparse: An Intermediate Language for General Sparse Format Customization. 137-165 - Ada Lamba, Max Taylor, Vincent Beardsley, Jacob Bambeck, Michael D. Bond
, Zhiqiang Lin:
Cocoon: Static Information Flow Control in Rust. 166-193 - Clement Blaudeau
, Didier Rémy, Gabriel Radanne:
Fulfilling OCaml Modules with Transparency. 194-222 - Anoud Alshnakat, Didrik Lundberg
, Roberto Guanciale, Mads Dam
:
HOL4P4: Mechanized Small-Step Semantics for P4. 223-249 - Shiv Sundram, Muhammad Usman Tariq, Fredrik Kjolstad
:
Compiling Recurrences over Dense and Sparse Arrays. 250-275 - Noam Zilberstein
, Angelina Saliling, Alexandra Silva:
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects. 276-304 - Di Wang
, Thomas W. Reps:
Newtonian Program Analysis of Probabilistic Programs. 305-333 - Kuang-Chen Lu
, Shriram Krishnamurthi
:
Identifying and Correcting Programming Language Behavior Misconceptions. 334-361 - Krishnendu Chatterjee
, Amir Kafshdar Goharshady, Tobias Meggendorfer
, Dorde Zikelic:
Quantitative Bounds on Resource Usage of Probabilistic Programs. 362-391 - Yangruibo Ding
, Marcus J. Min, Gail E. Kaiser
, Baishakhi Ray:
CYCLE: Learning to Self-Refine the Code Generation. 392-418 - Wolf Honoré
, Longfei Qiu
, Yoonseung Kim
, Ji-Yong Shin
, Jieung Kim
, Zhong Shao
:
AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. 419-448 - Ziyang Xu
, Yebin Chon, Yian Su
, Zujun Tan, Sotiris Apostolakis, Simone Campanoni
, David I. August:
PROMPT: A Fast and Extensible Memory Profiling Framework. 449-473 - Haonan Li
, Yu Hao
, Yizhuo Zhai, Zhiyun Qian:
Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach. 474-499 - Qian Chen, Chenyang Yu, Ruyan Liu, Chi Zhang
, Yu Wang, Ke Wang, Ting Su, Linzhang Wang
:
Evaluating the Effectiveness of Deep Learning Models for Foundational Program Analysis Tasks. 500-528 - Jonathan Castello
, Patrick Redmond, Lindsey Kuper
:
Inductive Diagrams for Causal Reasoning. 529-554 - Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon, Zhihao Jia:
Quarl: A Learning-Based Quantum Circuit Optimizer. 555-582 - Edward Lee, Yaoyu Zhao, Ondrej Lhoták, James You
, Kavin Satheeskumar, Jonathan Immanuel Brachthäuser
:
Qualifying System F<: Some Terms and Conditions May Apply. 583-612 - Tim Nelson, Ben Greenman
, Siddhartha Prasad
, Tristan Dyer
, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney Levine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, Shriram Krishnamurthi:
Forge: A Tool and Language for Teaching Formal Methods. 613-641 - Zhe Chen
, Yunlong Zhu, Zhemin Wang:
Design and Implementation of an Aspect-Oriented C Programming Language. 642-669 - Joseph W. Cutler
, Craig Disselkoen
, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks
, Kesha Hietala
, Eleftherios Ioannidis, John H. Kastner
, Anwar Mamat
, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew Wells:
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. 670-697 - Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang
, Nada Amin
:
Persimmon: Nested Family Polymorphism with Extensible Variant Types. 698-724 - Manasij Mukherjee, John Regehr:
Hydra: Generalizing Peephole Optimizations with Program Synthesis. 725-753 - Shigeyuki Sato
, Tomoki Nakamaru:
Multiverse Notebook: Shifting Data Scientists to Time Travelers. 754-783 - Martin Avanzini, Gilles Barthe
, Benjamin Grégoire
, Georg Moser
, Gabriele Vanoni
:
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. 784-809 - Gabriel Ryan
, Burcu Cetin, Yongwhan Lim, Suman Jana:
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning. 810-832 - Aaditya Naik
, Adam Stein, Yinjun Wu, Mayur Naik
, Eric Wong
:
TorchQL: A Programming Framework for Integrity Constraints in Machine Learning. 833-863 - Olek Gierczak, Lucy Menon, Christos Dimoulas
, Amal Ahmed
:
Gradually Typed Languages Should Be Vigilant! 864-892 - Jesse Michel, Kevin Mu, Xuanda Yang, Sai Praveen Bangaru
, Elias Rojas Collins, Gilbert Bernstein, Jonathan Ragan-Kelley
, Michael Carbin, Tzu-Mao Li:
Distributions for Compositionally Differentiating Parametric Discontinuities. 893-922 - Lutz Klinkenberg
, Christian Blumenthal
, Mingshuai Chen
, Darion Haase
, Joost-Pieter Katoen
:
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. 923-953 - Yifan Zhang, Yuanfeng Shi, Xin Zhang
:
Learning Abstraction Selection for Bayesian Program Analysis. 954-982 - David Binder
, Ingo Skupin, Tim Süberkrüb
, Klaus Ostermann
:
Deriving Dependently-Typed OOP from First Principles. 983-1009 - Anan Kabaha, Dana Drachsler-Cohen:
Verification of Neural Networks' Global Robustness. 1010-1039 - Daniel Marshall, Dominic Orchard
:
Functional Ownership through Fractional Uniqueness. 1040-1070 - Yang He, Pinhan Zhao
, Xinyu Wang
, Yuepeng Wang
:
VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints. 1071-1099 - Jialu Zhang, José Pablo Cambronero, Sumit Gulwani
, Vu Le
, Ruzica Piskac
, Gustavo Soares, Gust Verbruggen:
PyDex: Repairing Bugs in Introductory Python Assignments using LLMs. 1100-1124 - Joanna C. S. Santos
, Mehdi Mirakhorli
, Ali Shokri
:
Seneca: Taint-Based Call Graph Construction for Java Object Deserialization. 1125-1153 - Scott Smith, Robert Zhang:
A Pure Demand Operational Semantics with Applications to Program Analysis. 1154-1180 - Yichen Xu
, Aleksander Boruch-Gruszecki
, Martin Odersky
:
Degrees of Separation: A Flexible Type System for Safe Concurrency. 1181-1207 - Mingwei Zheng
, Qingkai Shi, Xuwei Liu
, Xiangzhe Xu
, Le Yu, Congyu Liu, Guannan Wei
, Xiangyu Zhang:
ParDiff: Practical Static Differential Analysis of Network Protocol Parsers. 1208-1234 - Amanda Stjerna
, Philipp Rümmer:
A Constraint Solving Approach to Parikh Images of Regular Languages. 1235-1263 - Zhaoyu Wang
, Pingchuan Ma, Huaijin Wang
, Shuai Wang
:
PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis. 1264-1293 - Constantin Enea, Eric Koskinen
:
Scenario-Based Proofs for Concurrent Objects. 1294-1323 - Yongjian Li
, Bohua Zhan
, Jun Pang:
Mechanizing the CMP Abstraction for Parameterized Verification. 1324-1350 - Ryan Kavanagh
, Brigitte Pientka
:
Message-Observing Sessions. 1351-1379 - Yifei Lu
, Weidong Hou, Minxue Pan, Xuandong Li, Zhendong Su
:
Understanding and Finding Java Decompiler Bugs. 1380-1406 - Qianchuan Ye
, Benjamin Delaware
:
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation. 1407-1436 - Pei Xu, Yuxiang Lei
, Yulei Sui, Jingling Xue:
Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability. 1437-1462 - Abhishek Rose, Sorav Bansal:
Modeling Dynamic (De)Allocations of Local Memory for Translation Validation. 1463-1492
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.