ESOP 2026

32 papers

1. A Category-Theoretic Framework for Dependent Effect Systems · Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno
2. A Formal Interface for Concurrent Search Structure Templates · Duc-Than Nguyen, William Mansky
3. A Formally Verified Procedure for Width Inference in FIRRTL · Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Fu Song, Taolue Chen + 1 more
4. A Program Logic for Under-approximating Worst-case Resource Usage · Ziyue Jin, Di Wang
5. Auditing Rust Crates Effectively · Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford
6. Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism · Hasti Toossi, Ningning Xie
7. Causal-Broadcast Memory · Amir Karniel, Ori Lahav
8. Code Generation via Meta-programming in Dependently Typed Proof Assistants · Mathis Bouverot-Dupuis, Yannick Forster
9. Complete Abstractions for Verification of Polymorphic Functions with Equality · Malo Revel, Thomas Genet, Thomas P. Jensen
10. Contextual Metaprogramming for Session Types · Pedro Ângelo, Atsushi Igarashi, Yuito Murase, Vasco T. Vasconcelos
11. Deciding not to Decide - Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism · Patrycja Balik, Szymon Jedras, Piotr Polesiuk
12. Denotational reasoning for asynchronous multiparty session types · Dylan McDermott, Nobuko Yoshida
13. Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs · Han Xu, Di Wang
14. Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search · Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh, Mahesh Vishwanathan
15. Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing · Philipp Schröer, Darion Haase, Joost-Pieter Katoen
16. Formal Methods meet Digital Twins: Challenges and Opportunities · Einar Broch Johnsen, Eduard Kamburjan, Andrea Pferscher, Silvia Lizeth Tapia Tarifa
17. Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops · Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg + 1 more
18. In Cantor Space No One Can Hear You Stream · Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot
19. Lenses for Partially-Specified States · Kazutaka Matsuda, Minh Nguyen, Meng Wang
20. Linear Effects, Exceptions, and Resource Safety - A Curry-Howard Correspondence for Destructors · Sidney Congard, Guillaume Munch-Maccagnoni, Rémi Douence
21. Max-Policy Iteration, Revisited · David Monniaux, Helmut Seidl
22. Modular Automatic Complexity Analysis of Recursive Integer Programs · Nils Lommen, Jürgen Giesl
23. Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT · Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz Del Valle, Alexandra Silva, Marco Gaboardi
24. Practical Refinement Session Type Inference · Toby Ueno, Ankush Das
25. Recursive Logical Relations for Intuitionistic Linear Logic Session Types · Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao
26. Reduction for Structured Concurrent Programs · Namratha Gangamreddypalli, Constantin Enea, Shaz Qadeer
27. Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators · Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi
28. Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction - · John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright
29. Specification-Driven Generation of Summaries for Symbolic Execution · Rafael Gonçalves, Frederico Ramos, Pedro Adão, José Fragoso Santos
30. Specifying and Verifying RDMA Synchronisation · Guillaume Ambal, Max Stupple, Brijesh Dongol, Azalea Raad
31. The Memorist Tale: Every Thunk Every Cost All At Once · Xing Li, Yao Li, Peter Schachte, Christine Rizkallah
32. Validating Quantum State Preparation Programs · Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett, Alex Potanin