- Neta Elad
, Oded Padon, Sharon Shoham:
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. Proc. ACM Program. Lang. 8(POPL): 970-1000 (2024) - Martin Elsman:
Explicit Effects and Effect Constraints in ReML. Proc. ACM Program. Lang. 8(POPL): 2370-2394 (2024) - Claudia Faggian, Daniele Pautasso, Gabriele Vanoni:
Higher Order Bayesian Networks, Exactly. Proc. ACM Program. Lang. 8(POPL): 2514-2546 (2024) - Azadeh Farzan, Dominik Klumpp, Andreas Podelski:
Commutativity Simplifies Proofs of Parameterized Programs. Proc. ACM Program. Lang. 8(POPL): 2485-2513 (2024) - Azadeh Farzan, Umang Mathur:
Coarser Equivalences for Causal Concurrency. Proc. ACM Program. Lang. 8(POPL): 911-941 (2024) - Justin Frank, Benjamin Quiring, Leonidas Lampropoulos:
Generating Well-Typed Terms That Are Not "Useless". Proc. ACM Program. Lang. 8(POPL): 2318-2339 (2024) - Dan Frumin, Amin Timany, Lars Birkedal:
Modular Denotational Semantics for Effects with Guarded Interaction Trees. Proc. ACM Program. Lang. 8(POPL): 332-361 (2024) - Adam T. Geller, Justin Frank, William J. Bowman:
Indexed Types for a Statically Safe WebAssembly. Proc. ACM Program. Lang. 8(POPL): 2395-2424 (2024) - Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proc. ACM Program. Lang. 8(POPL): 753-784 (2024) - Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper:
Decalf: A Directed, Effectful Cost-Aware Logical Framework. Proc. ACM Program. Lang. 8(POPL): 273-301 (2024) - Simon Guilloud, Viktor Kuncak:
Orthologic with Axioms. Proc. ACM Program. Lang. 8(POPL): 1150-1178 (2024) - Jens Oliver Gutsfeld, Markus Müller-Olm, Christoph Ohrem:
Deciding Asynchronous Hyperproperties for Recursive Programs. Proc. ACM Program. Lang. 8(POPL): 33-60 (2024) - Matthew Hague, Artur Jez, Anthony W. Lin:
Parikh's Theorem Made Symbolic. Proc. ACM Program. Lang. 8(POPL): 1945-1977 (2024) - 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. Proc. ACM Program. Lang. 8(POPL): 604-637 (2024) - Philippe Heim, Rayna Dimitrova:
Solving Infinite-State Games via Acceleration. Proc. ACM Program. Lang. 8(POPL): 1696-1726 (2024) - Brandon Hewer, Graham Hutton:
Quotient Haskell: Lightweight Quotient Types for All. Proc. ACM Program. Lang. 8(POPL): 785-815 (2024) - Chih-Duo Hong, Anthony W. Lin:
Regular Abstractions for Array Systems. Proc. ACM Program. Lang. 8(POPL): 638-666 (2024) - Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers:
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. Proc. ACM Program. Lang. 8(POPL): 1385-1417 (2024) - Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, Lizzie Hernandez:
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability. Proc. ACM Program. Lang. 8(POPL): 2456-2484 (2024) - Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi:
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. Proc. ACM Program. Lang. 8(POPL): 115-147 (2024) - Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu:
Algebraic Effects Meet Hoare Logic in Cubical Agda. Proc. ACM Program. Lang. 8(POPL): 1663-1695 (2024) - Thomas Koehler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer:
Guided Equality Saturation. Proc. ACM Program. Lang. 8(POPL): 1727-1758 (2024) - Shankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis, Omkar Tuppe:
On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability. Proc. ACM Program. Lang. 8(POPL): 1239-1268 (2024) - Ugo Dal Lago, Alexis Ghyselen:
On Model-Checking Higher-Order Effectful Programs. Proc. ACM Program. Lang. 8(POPL): 2610-2638 (2024) - Xiang Li, Xiangyu Zhou, Rui Dong, Yihong Zhang, Xinyu Wang:
Efficient Bottom-Up Synthesis for Programs with Local Variables. Proc. ACM Program. Lang. 8(POPL): 1540-1568 (2024) - Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich:
Internalizing Indistinguishability with Dependent Types. Proc. ACM Program. Lang. 8(POPL): 1298-1325 (2024) - Zhongkui Ma, Jiaying Li, Guangdong Bai:
ReLU Hull Approximation. Proc. ACM Program. Lang. 8(POPL): 2260-2287 (2024) - Rupak Majumdar, V. R. Sathiyanarayana:
Positive Almost-Sure Termination: Complexity and Proof Rules. Proc. ACM Program. Lang. 8(POPL): 1089-1117 (2024) - Konstantinos Mamouras, Agnishom Chattopadhyay:
Efficient Matching of Regular Expressions with Lookaround Assertions. Proc. ACM Program. Lang. 8(POPL): 2761-2791 (2024) - William Mansky, Ke Du:
An Iris Instance for Verifying CompCert C Programs. Proc. ACM Program. Lang. 8(POPL): 148-174 (2024)
