default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDProceedings of the ACM on Programming Languages, Volume 9
Volume 9, Number POPL, 2025
- Ian Erik Varatalu, Margus Veanes, Juhan P. Ernits:
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds. 1-32 - Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko:
Symbolic Automata: Omega-Regularity Modulo Theories. 33-66 - Louis Narmour, Tomofumi Yuki, Sanjay V. Rajopadhye:
Maximal Simplification of Polyhedral Reductions. 67-94 - Roland Leißa, Marcel Ullrich, Joachim Meyer, Sebastian Hack:
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age. 95-125 - Orpheas van Rooij, Robbert Krebbers:
Affect: An Affine Type and Effect System. 126-154 - Kengo Hirata, Chris Heunen:
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime. 155-182 - Yiyun Liu, Jonathan Chan, Stephanie Weirich:
Consistency of a Dependent Calculus of Indistinguishability. 183-209 - Joris Ceulemans, Andreas Nuyts, Dominique Devriese:
BiSikkel: A Multimode Logical Framework in Agda. 210-240 - Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein, Mae Milano:
Flo: A Semantic Foundation for Progressive Stream Processing. 241-270 - Ellie Y. Cheng, Eric Atkinson, Guillaume Baudart, Louis Mandel, Michael Carbin:
Inference Plans for Hybrid Particle Filtering. 271-299 - Max Vistrup, Michael Sammler, Ralf Jung:
Program Logics à la Carte. 300-331 - Vikraman Choudhury, Simon J. Gay:
The Duality of λ-Abstraction. 332-361 - Chris Martens, Robert J. Simmons, Michael Arntzenius:
Finite-Choice Logic Programming. 362-390 - Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran:
On Extending Incorrectness Logic with Backwards Reasoning. 391-415 - Jason Z. S. Hu, Brigitte Pientka:
A Dependent Type Theory for Meta-programming with Intensional Analysis. 416-445 - Patrick Cousot, Jeffery Wang:
Calculational Design of Hyperlogics by Abstract Interpretation. 446-478 - Neta Elad, Sharon Shoham:
Axe 'Em: Eliminating Spurious States with Induction Axioms. 479-508 - Giovanna Kobus Conrado, Adam Husted Kjelstrøm, Jaco van de Pol, Andreas Pavlogiannis:
Program Analysis via Multiple Context Free Language Reachability. 509-538 - Noam Zilberstein, Dexter Kozen, Alexandra Silva, Joseph Tassarotti:
A Demonic Outcome Logic for Randomized Nondeterminism. 539-568 - Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller:
Formal Foundations for Translational Separation Logic Verifiers. 569-599 - Cheng Zhang, Tobias Kappé, David E. Narváez, Nico Naus:
CF-GKAT: Efficient Validation of Control-Flow Transformations. 600-626 - Xiaojia Rao, Stefan Radziuk, Conrad Watt, Philippa Gardner:
Progressful Interpreters for Efficient WebAssembly Mechanisation. 627-655 - Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer:
Data Race Freedom à la Mode. 656-686 - Joomy Korkut, Kathrin Stark, Andrew W. Appel:
A Verified Foreign Function Interface between Coq and C. 687-717 - Balder ten Cate, Tobias Kappé:
Algebras for Deterministic Computation Are Inherently Incomplete. 718-744 - Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, Anton Varonka:
Simple Linear Loops: Algebraic Invariants and Applications. 745-771 - Eric Giovannini, Tingting Ding, Max S. New:
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory. 772-801 - Jacob Prinz, Henry Blanchette, Leonidas Lampropoulos:
Pantograph: A Fluid and Typed Structure Editor. 802-831 - Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, Phitchaya Mangpo Phothilimthana, Mohsen Lesani, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodík, Amit Sabne, Charith Mendis:
TensorRight: Automated Verification of Tensor Graph Rewrites. 832-863 - Daniel Gratzer:
A Modal Deconstruction of Löb Induction. 864-892 - Xaver Fabian, Marco Patrignani, Marco Guarnieri, Michael Backes:
Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks. 893-922 - Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukás Holík, Ondrej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai:
Verifying Quantum Circuits with Level-Synchronized Tree Automata. 923-953 - Litao Zhou, Bruno C. d. S. Oliveira:
QuickSub: Efficient Iso-Recursive Subtyping. 954-985 - Umang Mathur, David Mestel, Mahesh Viswanathan:
The Decision Problem for Regular First Order Theories. 986-1012 - Sergey Goncharov, Stelios Tsampas, Henning Urbat:
Abstract Operational Methods for Call-by-Push-Value. 1013-1039 - Thien Udomsrirungruang, Nobuko Yoshida:
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types. 1040-1071 - Matthew Amy, Joseph Lunderville:
Linear and Non-linear Relational Analyses for Quantum Program Optimization. 1072-1103 - Fabian Zaiser, Andrzej S. Murawski, C.-H. Luke Ong:
Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops. 1104-1135 - Naoki Kobayashi:
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus. 1136-1166 - Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire:
A Quantitative Probabilistic Relational Hoare Logic. 1167-1195 - Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal:
Approximate Relational Reasoning for Higher-Order Probabilistic Programs. 1196-1226 - Yingte Xu, Gilles Barthe, Li Zhou:
Automating Equational Proofs in Dirac Notation. 1227-1259 - Rini Banerjee, Kayvan Memarian, Dhruv C. Makwana, Christopher Pulte, Neel Krishnaswami, Peter Sewell:
Fulminate: Testing CN Separation-Logic Specifications in C. 1260-1292 - Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte:
Preservation of Speculative Constant-Time by Compilation. 1293-1325 - Yonghyun Kim, Minki Cho, Jaehyung Lee, Jinwoo Kim, Taeyoung Yoon, Youngju Song, Chung-Kil Hur:
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting. 1326-1354 - Roberto Giacobazzi, Francesco Ranzato:
The Best of Abstract Interpretations. 1355-1385 - Andrea Colledan, Ugo Dal Lago:
Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages. 1386-1416 - Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal:
Modelling Recursion and Probabilistic Choice in Guarded Type Theory. 1417-1445 - Nico Lehmann, Cole Kurashige, Nikhil Akiti, Niroop Krishnakumar, Ranjit Jhala:
Generic Refinement Types. 1446-1474 - Yongwei Yuan, Zhe Zhou, Julia Belyakova, Suresh Jagannathan:
Derivative-Guided Symbolic Execution. 1475-1505 - Sören van der Wall, Roland Meyer:
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations. 1506-1535 - Philippe Heim, Rayna Dimitrova:
Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis. 1536-1567 - Arthur Correnson, Bernd Finkbeiner:
Coinductive Proofs for Temporal Hyperliveness. 1568-1595 - Jack Liell-Cock, Sam Staton:
Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories. 1596-1626 - Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele Vanoni:
Interaction Equivalence. 1627-1656 - Donnacha Oisín Kidney, Nicolas Wu:
Formalising Graph Algorithms with Coinduction. 1657-1686 - Jan van Brügge, James McKinna, Andrei Popescu, Dmitriy Traytel:
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings. 1687-1718 - Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan:
Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning. 1719-1749 - Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, Lukasz Ziarek:
Semantic Logical Relations for Timed Message-Passing Protocols. 1750-1781 - Lena Verscht, Benjamin Lucien Kaminski:
A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests. 1782-1811 - Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, Chung-Kil Hur:
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems. 1812-1839 - Dhruv Nevatia, Si Liu, David A. Basin:
Reachability Analysis of the Domain Name System. 1840-1870 - Rupak Majumdar, V. R. Sathiyanarayana:
Sound and Complete Proof Rules for Probabilistic Termination. 1871-1902 - Yu Zhang, Jérémie Koenig, Zhong Shao, Yuting Wang:
Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. 1903-1933 - Chenyu Zhou, Yuzhou Fang, Jingbo Wang, Chao Wang:
An Incremental Algorithm for Algebraic Program Analysis. 1934-1961 - Clement Blaudeau, Didier Rémy, Gabriel Radanne:
Avoiding Signature Avoidance in ML Modules with Zippers. 1962-1991 - Qiyuan Xu, David Sanán, Zhe Hou, Xiaokun Luan, Conrad Watt, Yang Liu:
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules. 1992-2024 - Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham:
A Primal-Dual Perspective on Program Verification Algorithms. 2025-2056 - Yufan Cai, Zhe Hou, David Sanán, Xiaokun Luan, Yun Lin, Jun Sun, Jin Song Dong:
Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus. 2057-2089 - Pavel Golovin, Michalis Kokologiannakis, Viktor Vafeiadis:
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency. 2090-2117 - Shengyi Jiang, Chen Cui, Bruno C. d. S. Oliveira:
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types. 2118-2148 - Evgenii Moiseenko, Matteo Meluzzi, Innokentii Meleshchenko, Ivan Kabashnyi, Anton Podkopaev, Soham Chakraborty:
Relaxed Memory Concurrency Re-executed. 2149-2175 - Michael D. Adams, Eric Griffis, Thomas Porter, Sundara Vishnu Satish, Eric Zhao, Cyrus Omar:
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus. 2176-2204 - Ruifeng Xie, Tom Schrijvers, Zhenjiang Hu:
Biparsers: Exact Printing for Data Synchronisation. 2205-2231 - Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis:
Model Checking C/C++ with Mixed-Size Accesses. 2232-2252 - Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter:
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. 2253-2281 - George Zakhour, Pascal Weisenburger, Jahrim Gabriele Cesario, Guido Salvaneschi:
Dis/Equality Graphs. 2282-2305 - Taro Sekiyama, Hiroshi Unno:
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs. 2306-2336 - Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer:
Tail Modulo Cons, OCaml, and Relational Separation Logic. 2337-2363
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 2025-02-09 14:56 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:
