default search action
Proceedings of the ACM on Programming Languages, Volume 8
Volume 8, Number POPL, January 2024
- Pascal Bergsträßer
, Moses Ganardi
Ramsey Quantifiers in Linear Arithmetics. 1-32 - Jens Oliver Gutsfeld
Deciding Asynchronous Hyperproperties for Recursive Programs. 33-60 - Xueying Qin
Shoggoth: A Formal Foundation for Strategic Rewriting. 61-89 - A. R. Balasubramanian
Reachability in Continuous Pushdown VASS. 90-114 - Fuga Kawamata
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. 115-147 - William Mansky
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
Internal and Observational Parametricity for Cubical Agda. 209-240 - Amin Timany
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. 241-272 - Harrison Grodin
Decalf: A Directed, Effectful Cost-Aware Logical Framework. 273-301 - Alexandre Moine
DisLog: A Separation Logic for Disentanglement. 302-331 - Dan Frumin
Modular Denotational Semantics for Effects with Guarded Interaction Trees. 332-361 - Takeshi Tsukada
Enriched Presheaf Model of Quantum FPC. 362-392 - Guannan Wei
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
Optimal Program Synthesis via Abstract Interpretation. 457-481 - Francis Rinaldi
Pipelines and Beyond: Graph Types for ADTs with Futures. 482-511 - Noah Patton
Programming-by-Demonstration for Long-Horizon Robot Tasks. 512-545 - Jacques Carette
With a Few Square Roots, Quantum Computing Is as Easy as Pi. 546-574 - Amin Timany
The Logical Essence of Well-Bracketed Control Flow. 575-603 - Angus Hammond
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. 604-637 - Chih-Duo Hong
Regular Abstractions for Array Systems. 638-666 - Will Crichton
A Core Calculus for Documents: Or, Lambda: The Ultimate Document. 667-694 - Filip Sieczkowski
The Essence of Generalized Algebraic Data Types. 695-723 - John Cyphert
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis. 724-752 - Simon Oddershede Gregersen
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. 753-784 - Brandon Hewer
Quotient Haskell: Lightweight Quotient Types for All. 785-815 - Shankara Pailoor
Semantic Code Refactoring for Abstract Data Types. 816-847 - Pu Sun
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis. 848-881 - Julian Müllner
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. 882-910 - Azadeh Farzan
Coarser Equivalences for Causal Concurrency. 911-941 - Ian Briggs
Implementation and Synthesis of Math Library Functions. 942-969 - Neta Elad
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. 970-1000 - Alex Buna-Marginean
On Learning Polynomial Recursive Programs. 1001-1027 - Jianan Yao
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions. 1028-1059 - Tom Smeding
Efficient CHAD. 1060-1088 - Rupak Majumdar
Positive Almost-Sure Termination: Complexity and Proof Rules. 1089-1117 - Sam Westrick
Automatic Parallelism Management. 1118-1149 - Simon Guilloud
Orthologic with Axioms. 1150-1178 - Giuseppe Castagna
Polymorphic Type Inference for Dynamic Languages. 1179-1210 - Xing Zhang
Fusing Direct Manipulations into Functional Programs. 1211-1238 - Shankaranarayanan Krishna
On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability. 1239-1268 - Lorenzo Ceragioli
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers. 1269-1297 - Yiyun Liu
Internalizing Indistinguishability with Dependent Types. 1298-1325 - Mikolaj Bojanczyk
Polyregular Functions on Unordered Trees of Bounded Height. 1326-1351 - Liron Cohen
The Complex(ity) Landscape of Checking Infinite Descent. 1352-1384 - Jules Jacobs
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. 1385-1417 - Lionel Parreaux
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism. 1418-1450 - Lyes Attouche
Validation of Modern JSON Schema: Formalization and Complexity. 1451-1481 - François Pottier
Thunks and Debits in Separation Logic with Time Credits. 1482-1508 - Nicolas Chataing
Unboxed Data Constructors: Or, How cpp Decides a Halting Problem. 1509-1539 - Xiang Li
Efficient Bottom-Up Synthesis for Programs with Local Variables. 1540-1568 - Jatin Arora
Disentanglement with Futures, State, and Interaction. 1569-1599 - Wenhao Tang
Soundly Handling Linearity. 1600-1628 - Marco Campion
Monotonicity and the Precision of Program Analysis. 1629-1662 - Donnacha Oisín Kidney
Algebraic Effects Meet Hoare Logic in Cubical Agda. 1663-1695 - Philippe Heim
Solving Infinite-State Games via Acceleration. 1696-1726 - Thomas Koehler
Guided Equality Saturation. 1727-1758 - Haowei Deng
A Case for Synthesis of Recursive Quantum Unitary Programs. 1759-1788 - Joshua M. Cohen
A Formalization of Core Why3 in Coq. 1789-1818 - Nathanael L. Ackerman
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets. 1819-1849 - Thodoris Sotiropoulos
API-Driven Program Synthesis for Testing Static Typing Implementations. 1850-1881 - Francesca Randone
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures. 1882-1912 - Itsaka Rakotonirina
Decision and Complexity of Dolev-Yao Hyperproperties. 1913-1944 - Matthew Hague
Parikh's Theorem Made Symbolic. 1945-1977 - Soham Chakraborty
How Hard Is Weak-Memory Testing? 1978-2009 - Steven Ramsay
Ill-Typed Programs Don't Evaluate. 2010-2040 - Eric Zhao
Total Type Error Localization and Recovery with Holes. 2041-2068 - Litao Zhou
VST-A: A Foundationally Sound Annotation Verifier. 2069-2098 - Michael Borkowski
Mechanizing Refinement Types. 2099-2128 - Yuantian Ding
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations. 2129-2159 - Ling Zhang
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. 2160-2190 - Zhendong Ang
Predictive Monitoring against Pattern Regular Languages. 2191-2225 - Cezar-Constantin Andrici
Securing Verified IO Programs Against Unverified Code in F. 2226-2259 - Zhongkui Ma
ReLU Hull Approximation. 2260-2287 - Robert Atkey
Polynomial Time and Dependent Types. 2288-2317 - Justin Frank
Generating Well-Typed Terms That Are Not "Useless". 2318-2339 - Thorsten Altenkirch
Internal Parametricity, without an Interval. 2340-2369 - Martin Elsman
Explicit Effects and Effect Constraints in ReML. 2370-2394 - Adam T. Geller
Indexed Types for a Statically Safe WebAssembly. 2395-2424 - Yuxiang Peng
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation. 2425-2455 - Prasad Jayanti
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability. 2456-2484 - Azadeh Farzan
Commutativity Simplifies Proofs of Parameterized Programs. 2485-2513 - Claudia Faggian
Higher Order Bayesian Networks, Exactly. 2514-2546 - Conrad Zimmerman
Sound Gradual Verification with Symbolic Execution. 2547-2576 - Supun Abeysinghe
Flan: An Expressive and Efficient Datalog Compiler for Program Analysis. 2577-2609 - Ugo Dal Lago
On Model-Checking Higher-Order Effectful Programs. 2610-2638 - Cameron Moy
Effectful Software Contracts. 2639-2666 - John Peter Campora III
Type-Based Gradual Typing Performance Optimization. 2667-2699 - Henry DeYoung
Parametric Subtyping for Structural Parametric Polymorphism. 2700-2730 - Yanis Sellami
Inference of Robust Reachability Constraints. 2731-2760 - Konstantinos Mamouras
Efficient Matching of Regular Expressions with Lookaround Assertions. 2761-2791 - Kevin Batz
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. 2792-2820
Volume 8, Number PLDI, 2024
- Debangshu Banerjee
Input-Relational Verification of Deep Neural Networks. 1-27 - Minseong Jang
Modular Hardware Design of Pipelined Circuits with Hazards. 28-51 - Yannick Forster
Verified Extraction from Coq to OCaml. 52-75 - Long Pham
Robust Resource Bounds with Static Analysis and Bayesian Inference. 76-101 - Qiantan Hong
Recursive Program Synthesis using Paramorphisms. 102-125 - Aleksandar Krastev
A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption. 126-150 - Jaehwang Jung
Concurrent Immediate Reference Counting. 151-174 - Sunho Park
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. 175-198 - Siva Kesava Reddy Kakarla
Diffy: Data-Driven Bug Finding for Configurations. 199-222 - Shaohua Li
Boosting Compiler Testing by Injecting Real-World Code. 223-245 - Benjamin Mikek
SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories. 246-271 - Ritvik Sharma
Compilation of Qubit Circuits to Optimized Qutrit Circuits. 272-295 - Aditya Anand
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes. 296-319 - Amanda Liu
A Verified Compiler for a Functional Tensor Language. 320-342 - Chujun Geng
IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications. 343-367 - Dorian Lesbre
Compiling with Abstract Interpretation. 368-393 - Matthew Lutze
Associated Effects: Flexible Abstractions for Effectful Programming. 394-416 - Mafalda Ferreira
Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs. 417-441 - Joao Rivera
Floating-Point TVPI Abstract Domain. 442-466 - Ajay Brahmakshatriya
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks. 467-491 - Charles Yuan
The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation. 492-517 - Anton Lorenzen
The Functional Essence of Imperative Binary Search Trees. 518-542 - Mikhail Svyatlovskiy
Compositional Semantics for Shared-Variable Concurrency. 543-566 - Peisen Yao
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis. 567-592 - Hongzheng Chen
Allo: A Programming Model for Composable Accelerator Design. 593-620 - Joseph Raskind
VESTA: Power Modeling with Language Runtime Events. 621-646 - Vladimir Gladshtein
Mechanised Hypersafety Proofs about Structured Data. 647-670 - Theodoros Theodoridis
Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior. 671-691 - Thomas Ball
Jacdac: Service-Based Prototyping of Embedded Systems. 692-715 - Jaemin Hong
Don't Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation. 716-740 - Guillaume Girol
Quantitative Robustness for Vulnerability Assessment. 741-765 - George Zakhour
Automated Verification of Fundamental Algebraic Laws. 766-789 - Mathieu Huot
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables. 790-815 - Iavor S. Diatchki
Daedalus: Safer Document Parsing. 816-840 - Bastian Köpcke
Descend: A Safe GPU Systems Programming Language. 841-864 - Poorva Garg
Bit Blasting Probabilistic Programs. 865-888 - Simon Spies
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. 889-913 - Jiawen Liu
Program Analysis for Adaptive Data Analysis. 914-938 - Ruyi Ji
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. 939-964 - Guannan Wei
Consolidating Smart Contracts with Behavioral Contracts. 965-989 - Christian Wimmer
Scaling Type-Based Points-to Analysis with Saturation. 990-1013 - Ziteng Wang
From Batch to Stream: Automatic Generation of Online Algorithms. 1014-1039 - Wang Fang
Symbolic Execution for Quantum Error Correction Programs. 1040-1065 - Blake Pelton
Wavefront Threading Enables Effective High-Level Synthesis. 1066-1090 - Julia Belyakova
Decidable Subtyping of Existential Types for Julia. 1091-1114 - Lennard Gäher
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. 1115-1139 - Longfei Qiu
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. 1140-1164 - Mathias Rud Laursen
Reducing Static Analysis Unsoundness with Approximate Interpretation. 1165-1188 - Parosh Aziz Abdulla
Verification under Intel-x86 with Persistency. 1189-1212 - Genghan Zhang
Compilation of Modular and General Sparse Workspaces. 1213-1238 - Mridul Aanjaneya
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
A Lightweight Polyglot Code Transformation Language. 1288-1312 - Anita Buckley
An Algebraic Language for Specifying Quantum Networks. 1313-1335 - Aurèle Barrière
Linear Matching of JavaScript Regular Expressions. 1336-1360 - Peixin Wang
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. 1361-1386 - Zhe Zhou
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata. 1387-1411 - Joseph W. Cutler
Stream Types. 1412-1436 - Elvira Albert
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. 1437-1462 - Keli Huang
Compiling Conditional Quantum Gates without Using Helper Qubits. 1463-1484 - Thibault Dardinier
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. 1485-1509 - Gaurav Parthasarathy
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. 1510-1534 - Samuel Gruetter
Live Verification in an Interactive Proof Assistant. 1535-1558 - Dongjun Youn
Bringing the WebAssembly Standard up to Speed with SpecTec. 1559-1584 - Atsushi Igarashi
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric. 1585-1608 - Tianyu Chen
Quest Complete: The Holy Grail of Gradual Security. 1609-1632 - Qiuping Yi
Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding. 1633-1655 - Michael Fitzgibbons
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. 1656-1679 - Avery Laird
SpEQ: Translation of Sparse Codes using Equivalences. 1680-1703 - Andres Erbsen
Foundational Integration Verification of a Cryptographic Server. 1704-1729 - Guofeng Cui
Reward-Guided Synthesis of Intelligent Agents with Control Structures. 1730-1754 - Jianlin Li
Compiling Probabilistic Programs for Variable Elimination with Information Flow. 1755-1780 - Michalis Kokologiannakis
SPORE: Combining Symmetry and Partial Order Reduction. 1781-1803 - Adithya Murali
Predictable Verification using Intrinsic Definitions. 1804-1829 - Yuxiang Lei
Context-Free Language Reachability via Skewed Tabulation. 1830-1853 - Arjun Pitchanathan
Falcon: A Scalable Analytical Cache Model. 1854-1878 - Justin Lubin
Equivalence by Canonicalization for Synthesis-Backed Refactoring. 1879-1904 - Mark Moeller
KATch: A Fast Symbolic Verifier for NetKAT. 1905-1928 - Yann Herklotz
Hyperblock Scheduling for Verified High-Level Synthesis. 1929-1953 - Ariel E. Kellison
Numerical Fuzz: A Type System for Rounding Error Analysis. 1954-1978 - Takeshi Tsukada
Inductive Approach to Spacer. 1979-2002 - Xiaodong Jia
V-Star: Learning Visibly Pushdown Grammars from Program Inputs. 2003-2026 - Lasse Blaauwbroek
Hashing Modulo Context-Sensitive 𝛼-Equivalence. 2027-2050 - Gabriel Matute
Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments. 2051-2072 - Konstantinos Mamouras
Static Analysis for Checking the Disambiguation Robustness of Regular Expressions. 2073-2097 - Krishnendu Chatterjee
Equivalence and Similarity Refutation for Probabilistic Programs. 2098-2122 - McCoy R. Becker
Probabilistic Programming with Programmable Variational Inference. 2123-2147 - Minseok Jeon
PL4XGL: A Programming Language Approach to Explainable Graph Learning. 2148-2173 - Ruslan Nikolaev
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation. 2174-2198
Volume 8, Number OOPSLA1, 2024
- Charles Yuan
Quantum Control Machine: The Limits of Control Flow in Quantum Programming. 1-28 - Will Crichton
Profiling Programming Language Learning. 29-54 - Anouk Paradis, Jasper Dekoninck
Synthetiq: Fast and Versatile Quantum Circuit Synthesis. 55-82 - Aashish Yadavally
A Learning-Based Approach to Static Program Slicing. 83-109 - Chi Zhang
Finding Cross-Rule Optimization Bugs in Datalog Engines. 110-136 - Jie Liu
UniSparse: An Intermediate Language for General Sparse Format Customization. 137-165 - Ada Lamba
Cocoon: Static Information Flow Control in Rust. 166-193 - Clement Blaudeau
Fulfilling OCaml Modules with Transparency. 194-222 - Anoud Alshnakat, Didrik Lundberg
HOL4P4: Mechanized Small-Step Semantics for P4. 223-249 - Shiv Sundram, Muhammad Usman Tariq
Compiling Recurrences over Dense and Sparse Arrays. 250-275 - Noam Zilberstein
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects. 276-304 - Di Wang
Newtonian Program Analysis of Probabilistic Programs. 305-333 - Kuang-Chen Lu
Identifying and Correcting Programming Language Behavior Misconceptions. 334-361 - Krishnendu Chatterjee
Quantitative Bounds on Resource Usage of Probabilistic Programs. 362-391 - Yangruibo Ding
CYCLE: Learning to Self-Refine the Code Generation. 392-418 - Wolf Honoré
AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. 419-448 - Ziyang Xu
PROMPT: A Fast and Extensible Memory Profiling Framework. 449-473 - Haonan Li
Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach. 474-499 - Qian Chen, Chenyang Yu, Ruyan Liu, Chi Zhang
Evaluating the Effectiveness of Deep Learning Models for Foundational Program Analysis Tasks. 500-528 - Jonathan Castello
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
Qualifying System F<: Some Terms and Conditions May Apply. 583-612 - Tim Nelson, Ben Greenman
Forge: A Tool and Language for Teaching Formal Methods. 613-641 - Zhe Chen
Design and Implementation of an Aspect-Oriented C Programming Language. 642-669 - Joseph W. Cutler
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. 670-697 - Anastasiya Kravchuk-Kirilyuk
Persimmon: Nested Family Polymorphism with Extensible Variant Types. 698-724 - Manasij Mukherjee
Hydra: Generalizing Peephole Optimizations with Program Synthesis. 725-753 - Shigeyuki Sato
Multiverse Notebook: Shifting Data Scientists to Time Travelers. 754-783 - Martin Avanzini, Gilles Barthe
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. 784-809 - Gabriel Ryan
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning. 810-832 - Aaditya Naik
TorchQL: A Programming Framework for Integrity Constraints in Machine Learning. 833-863 - Olek Gierczak
Gradually Typed Languages Should Be Vigilant! 864-892 - Jesse Michel
Distributions for Compositionally Differentiating Parametric Discontinuities. 893-922 - Lutz Klinkenberg
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. 923-953 - Yifan Zhang
Learning Abstraction Selection for Bayesian Program Analysis. 954-982 - David Binder
Deriving Dependently-Typed OOP from First Principles. 983-1009 - Anan Kabaha, Dana Drachsler-Cohen:
Verification of Neural Networks' Global Robustness. 1010-1039 - Danielle Marshall
Functional Ownership through Fractional Uniqueness. 1040-1070 - Yang He
VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints. 1071-1099 - Jialu Zhang
PyDex: Repairing Bugs in Introductory Python Assignments using LLMs. 1100-1124 - Joanna C. S. Santos
Seneca: Taint-Based Call Graph Construction for Java Object Deserialization. 1125-1153 - Scott Smith
A Pure Demand Operational Semantics with Applications to Program Analysis. 1154-1180 - Yichen Xu
Degrees of Separation: A Flexible Type System for Safe Concurrency. 1181-1207 - Mingwei Zheng
ParDiff: Practical Static Differential Analysis of Network Protocol Parsers. 1208-1234 - Amanda Stjerna
A Constraint Solving Approach to Parikh Images of Regular Languages. 1235-1263 - Zhaoyu 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
Mechanizing the CMP Abstraction for Parameterized Verification. 1324-1350 - Ryan Kavanagh
Message-Observing Sessions. 1351-1379 - Yifei Lu
Understanding and Finding Java Decompiler Bugs. 1380-1406 - Qianchuan Ye
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation. 1407-1436 - Pei Xu
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
Volume 8, Number ICFP, 2024
- Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry:
How to Bake a Quantum Π. 1-29 - Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, Yao Li:
Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs. 30-63 - Michael Ballantyne, Mitch Gamburg, Jason Hemann:
Compiled, Extensible, Multi-language DSLs (Functional Pearl). 64-87 - Martin Elsman:
Double-Ended Bit-Stealing for Algebraic Data Types. 88-120 - Guillaume Melquiond, Josué Moreau:
A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler. 121-146 - Paulo Torrens, Dominic Orchard, Cristiano D. Vasconcellos:
On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs. 147-176 - Manuel Serrano, Robert Bruce Findler:
The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl). 177-202 - Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Almost-Sure Termination by Guarded Refinement. 203-233 - Atze Dijkstra, José Pedro Magalhães, Pierre Néron:
Functional Programming in Financial Markets (Experience Report). 234-248 - Yijia Chen, Lionel Parreaux:
The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures. 249-283 - Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. 284-316 - Niek Mulleners
Example-Based Reasoning about the Realizability of Polymorphic Programs. 317-337 - Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer:
Snapshottable Stores. 338-369 - Patrick Bahr, Graham Hutton:
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl). 370-394 - David Binder, Marco Tzschentke, Marius Müller, Klaus Ostermann:
Grokking the Sequent Calculus (Functional Pearl). 395-425 - Son Ho, Aymeric Fromherz, Jonathan Protzenko:
Sound Borrow-Checking for Rust via Symbolic Semantics. 426-454 - Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi:
Abstracting Effect Systems for Algebraic Effect Handlers. 455-484 - Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, Sam Lindley:
Oxidizing OCaml with Modal Memory Management. 485-514 - Bram Vandenbogaerde, Quentin Stiévenart, Coen De Roover:
Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts. 515-543 - Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter:
Gradual Indexed Inductive Types. 544-572 - Youngju Song, Dongjae Lee:
Refinement Composition Logic. 573-601 - Sébastien Michelland, Yannick Zakowski, Laure Gonnord:
Abstract Interpreters: A Monadic Approach to Modular Verification. 602-629 - Théo Winterhalter:
Dependent Ghosts Have a Reflection for Free. 630-658 - András Kovács:
Closure-Free Functional Programming in a Two-Level Type Theory. 659-692 - Tsung-Ju Chiang
Staged Compilation with Module Functors. 693-727 - Benjamin Quiring, David Van Horn:
Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis. 728-755 - Ningning Xie, Daniel D. Johnson, Dougal Maclaurin, Adam Paszke:
Parallel Algebraic Effect Handlers. 756-788 - Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic:
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. 789-817 - Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova:
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. 818-844 - Paul Downen
Call-by-Unboxed-Value. 845-879 - Xu Xue
Contextual Typing. 880-908 - Yahui Song, Darius Foo, Wei-Ngan Chin:
Specification and Verification for Unrestricted Algebraic Effects and Handling. 909-937 - Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Ayele, Bereket Ngussie Bekele, Shayan Jalili, Pranjal Sharma
Synchronous Programming with Refinement Types. 938-972 - Satoshi Kura, Hiroshi Unno:
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System. 973-1002 - Noé De Santo, Aurèle Barrière, Clément Pit-Claudel:
A Coq Mechanization of JavaScript Regular Expression Semantics. 1003-1031
Volume 8, Number OOPSLA2, 2024
- Yichuan Li
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts. 1-29 - Julien Simonnet
A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code. 30-59 - David Klopp
Object-Oriented Fixpoint Programming with Datalog. 60-86 - Zachary Palmer
Intensional Functions. 87-112 - Shaan Nagy
Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs. 113-139 - Chan Gu Kang
Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification. 140-164 - William J. Bowman
A Low-Level Look at A-Normal Form. 165-191 - Litao Zhou
Full Iso-Recursive Types. 192-221 - Chengyu Zhang
SMT2Test: From SMT Formulas to Effective Test Cases. 222-245 - Azalea Raad
Non-termination Proving at Scale. 246-274 - Peiming Liu
Compiler Support for Sparse Tensor Convolutions. 275-303 - Maxime Legoupil
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly. 304-332 - Jos Craaijo
libLISA: Instruction Discovery and Analysis on x86-64. 333-361 - Jiangyi Liu
Synthesizing Formal Semantics from Executable Interpreters. 362-388 - Vineet Rajani
A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs. 389-414 - Elisabet Lobo Vesga
Sensitivity by Parametricity. 415-441 - Luke Geeson
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations. 442-467 - Andrew Blinn
Statically Contextualizing Large Language Models with Typed Holes. 468-498 - Zhengyao Lin
FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions. 499-526 - Adhitha Dias
SparseAuto: An Auto-scheduler for Sparse Tensor Computations using Recursive Loop Nest Restructuring. 527-556 - Seungmin Jeon
Quantum Probabilistic Model Checking for Time-Bounded Properties. 557-587 - Thomas Somers
Verified Lock-Free Session Channels with Linking. 588-617 - Yoshiki Takashima
Crabtree: Rust API Test Synthesis Guided by Coverage and Type. 618-647 - Wenjia Ye
Merging Gradual Typing. 648-676 - Federico Cassano
Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs. 677-708 - Chenyuan Yang
WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Models. 709-735 - Michael Jungmair
HiPy: Extracting High-Level Semantics from Python Code for Data Processing. 736-762 - Loris D'Antoni
Automatically Reducing Privilege for Access Control Policies. 763-790 - Ziteng Yang
Fully Verified Instruction Scheduling. 791-816 - Linpeng Zhang
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers. 817-845 - Ethan Chen
CoolerSpace: A Language for Physically Correct and Computationally Efficient Color Programming. 846-875 - Si Liu
Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels. 876-904 - Eric Hayden Campbell
Computing Precise Control Interface Specifications. 905-934 - Keith J. C. Johnson
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics. 935-961 - Robin Webbers
Refinement Type Refutations. 962-987 - Luyu Cheng
The Ultimate Conditional Syntax. 988-1017 - Paul Maximilian Bittner
On the Expressive Power of Languages for Static Variability. 1018-1050 - Long Pham
Programmable MCMC with Soundly Composed Guide Programs. 1051-1080 - Paulo Emílio de Vilhena
Extending the C/C++ Memory Model with Inline Assembly. 1081-1107 - Cassia Torczon
Effects and Coeffects in Call-by-Push-Value. 1108-1134 - Aleksander Boruch-Gruszecki
Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types. 1135-1161 - Alexander J. Root
Compilation of Shape Operators on Sparse Arrays. 1162-1188 - Philipp G. Haselwarter
Tachis: Higher-Order Separation Logic with Credits for Expected Costs. 1189-1218 - Aaron Bembenek
Making Formulog Fast: An Argument for Unconventional Datalog Evaluation. 1219-1248 - Andrew Wagner
Realistic Realizability: Specifying ABIs You Can Count On. 1249-1278 - Thibault Dardinier
Hypra: A Deductive Program Verifier for Hyper Hoare Logic. 1279-1308 - Chijin Zhou
PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting. 1309-1335 - Zhichao Guan
Semantics Lifting for Syntactic Sugar. 1336-1361 - Boyao Ding
MEA2: A Lightweight Field-Sensitive Escape Analysis with Points-to Calculation for Golang. 1362-1389 - Meghana Sistla
Weighted Context-Free-Language Ordered Binary Decision Diagrams. 1390-1419 - Arthur Correnson
Finding ∀∃ Hyperbugs using Symbolic Execution. 1420-1445 - Jonas Kastberg Hinrichsen
Multris: Functional Verification of Multiparty Message Passing in Separation Logic. 1446-1474 - Hannes Saffrich
Law and Order for Typestate with Borrowing. 1475-1503 - Xin Yi
FPCC: Detecting Floating-Point Errors via Chain Conditions. 1504-1531 - Zhenyu Yan
Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks. 1532-1560 - Zhengyang Liu
Minotaur: A SIMD-Oriented Synthesizing Superoptimizer. 1561-1585 - David Klopp
A Typed Multi-level Datalog IR and Its Compiler Framework. 1586-1614 - Yiyu Zhang
HardTaint: Production-Run Dynamic Taint Analysis via Selective Hardware Tracing. 1615-1640 - David Schwartz
Jmvx: Fast Multi-threaded Multi-version Execution and Record-Replay for Managed Languages. 1641-1669 - Cong Ma
Lexical Effect Handlers, Directly. 1670-1698 - Alexis Le Glaunec
HybridSA: GPU Acceleration of Multi-pattern Regex Matching using Bit Parallelism. 1699-1728 - Jeff Eymer
A Runtime System for Interruptible Query Processing: When Incremental Computing Meets Fine-Grained Parallelism. 1729-1756 - Antonin Reitz
StarMalloc: Verifying a Modern, Hardened Memory Allocator. 1757-1786 - Robert Schenck
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming. 1787-1813 - Callista Le
Concurrent Data Structures Made Easy. 1814-1842 - Ningke Li
Drowzee: Metamorphic Testing for Fact-Conflicting Hallucination Detection in Large Language Models. 1843-1872 - Nikhil Pimpalkhare
Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials. 1873-1899 - Constantin Enea
Model Checking Distributed Protocols in Must. 1900-1927 - Andrea Borgarelli
Reward Augmentation in Reinforcement Learning for Testing Distributed Systems. 1928-1954 - Qian Wang
Rustlantis: Randomized Differential Testing of the Rust Compiler. 1955-1981 - Guillaume Ambal
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures. 1982-2009 - Wenjia Ye
Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing. 2010-2039 - Jifeng Wu
QuAC: Quick Attribute-Centric Type Inference for Python. 2040-2069 - Georgian-Vlad Saioc
Automated Verification of Parametric Channel-Based Process Communication. 2070-2096 - Hristo Venev
Modular Synthesis of Efficient Quantum Uncomputation. 2097-2124 - Denis Carnier
Type Inference Logics. 2125-2155 - Doehyun Baek
Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks. 2156-2182 - Kelvin Qian
Semantic-Type-Guided Bug Finding. 2183-2210 - Benjamin Mariano
Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis. 2211-2241 - Caleb Kim
Unifying Static and Dynamic Intermediate Languages for Accelerator Generators. 2242-2267 - Jonas Norlinder
Mark-Scavenge: Waiting for Trash to Take Itself Out. 2268-2295 - Arthur Oliveira Vale
Compositionality and Observational Refinement for Linearizability with Crashes. 2296-2324 - Augustine Wong
Making Sense of Multi-threaded Application Performance at Scale with NonSequitur. 2325-2354 - Chen Yang
Dependency-Aware Code Naturalness. 2355-2377 - Dominik Winterer
Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration. 2378-2401 - Shelly Grossman
Practical Verification of Smart Contracts using Memory Splitting. 2402-2433 - Dennis Liew
Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs. 2434-2461 - Mario Alvarez-Picallo
Effect Handlers for C via Coroutines. 2462-2489 - Georgios-Petros Drosos
When Your Infrastructure Is a Buggy Program: Understanding Faults in Infrastructure as Code Ecosystems. 2490-2520 - Jinhao Tan
A Case for First-Class Environments. 2521-2550 - Amir Kafshdar Goharshady
Fast and Optimal Extraction for Sparse Equality Graphs. 2551-2577 - Kartik Nagar
Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models. 2578-2605 - Shashin Halalingaiah
The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and Efficiently. 2606-2632 - Haofeng Li
Boosting the Performance of Alias-Aware IFDS Analysis with CFL-Based Environment Transformers. 2633-2661 - Taro Sekiyama
Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification. 2662-2691
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.
last updated on 2024-12-26 00:55 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: