default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDProceedings 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