ESOP 2026

ESOP seeks contributions on all aspects of programming language research including, but not limited to, the following areas:

• programming paradigms and styles
• methods and tools to specify and reason about programs and languages
• programming language foundations
• methods and tools for implementation, concurrency and distribution
• applications and emerging topics

Contributions bridging the gap between theory and practice are particularly welcome.

Please find a list of accepted papers below:

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

Round 1:

• Submission deadline: June 3, 2025
• Rebuttal: July 21-23, 2025
• Notification: August 1, 2025

Round 2:

• Submission deadline: October 16, 2025
• Rebuttal: December 8-10, 2025
• Notification: December 22, 2025

Please note that the deadlines are firm and will not be extended!

The important dates are available in the Joint Call for Papers.

ESOP 2026 solicits three forms of contributions:

• Research Papers are articles that advance the state-of-the-art on the theory and practice of programming languages and systems.
  For the sake of flexibility, submitted research papers may be formatted in Springer’s LNCS, ACM’s PACMPL, or ACM’s TOPLAS format. There is no page limit for submissions, but authors should be aware that reviewers are likely to balance the review time for all papers and that camera-ready papers may not exceed 25 pages (excluding bibliography) and must be formatted in Springer’s LNCS.
• Experience Reports are articles reporting on systems and techniques developed in practice, such as artifacts, tools, mechanized proofs, and educational systems, both in academic and industrial settings. These articles must include a critical evaluation of the experience reported. Submitted and camera-ready experience report papers must be formatted in Springer’s LNCS, not exceeding 15 pages (excluding bibliography).
• Fresh Perspectives are articles that promote new insights on programming languages and systems in a particularly elegant way. These papers may offer new tutorial perspectives of known concepts, or they may introduce fresh new insights and ideas that could lead to relevant future developments. Submitted and camera-ready fresh perspective papers must be formatted in Springer’s LNCS, not exceeding 15 pages (excluding bibliography).

The paper review process will be double-blind. Authors must make a good faith effort to anonymize their submissions, and they should not identify themselves either explicitly or by implication (e.g., through the references or acknowledgments).

Accepted papers will be published in Springer’s Lecture Notes in Computer Science series. Springer’s formatting style files and other information can be found on the Springer website.

The papers can be submitted here.

We welcome paper submissions at both submission rounds. Submissions of each round will be reviewed by the PC and external reviewers for their technical soundness and originality.

Round 1 submissions will receive one of three outcomes: Accept, Reject, Revise. In the latter case, the PC will provide a concrete list of revision requests to be completed by the Round 2 submission deadline. Such revised submissions will be reviewed by the same set of reviewers and will either be accepted or rejected. Rejected Round 1 submissions may NOT be resubmitted to Round 2.

Papers submitted directly to Round 2 will either be accepted or rejected.

ESOP 2026 will have a post-paper-acceptance voluntary artifact evaluation. Authors will be encouraged to submit artifacts for evaluation after paper notification. The outcome will not alter the paper acceptance decision.

Detailed information can be found here.

PC Chair

• Robbert Krebbers (Radboud University Nijmegen, Netherlands)

PC Members

• Alasdair Armstrong (University of Cambridge, UK)
• Aslan Askarov (Aarhus University, Denmark)
• Mohamed Faouzi Atig (Uppsala University, Sweden)
• Andrej Bauer (University of Ljubljana, Slovenia)
• Veronique Benzaken (LMF Université Paris-Saclay, France)
• Małgorzata Biernacka (University of Wrocław, Poland)
• Liang-Ting Chen (Academia Sinica, Taiwan)
• Raphaëlle Crubillé (Aix Marseille Univ, CNRS, LIS, France)
• Deepak D'Souza (Indian Institute of Science, India)
• Ankush Das (Boston University, USA)
• Farzaneh Derakhshan (Illinois Institute of Technology, USA)
• Emanuele D’Osualdo (University of Konstanz, Germany)
• Paulo Emílio de Vilhena (Imperial College London, UK)
• Francesco Gavazzo (University of Padua, Italy)
• Justin Hsu (Cornell University, USA)
• Ambrus Kaposi (Eötvös Loránd University, Hungary)
• Sven Keidel (TU Darmstadt, Germany)
• Ori Lahav (Tel Aviv University, Israel)
• Christoph Matheja (University of Oldenburg and DTU Compute, Germany)
• Andreia Mordido (LASIGE, University of Lisbon, Portugal)
• Christopher Pulte (University of Cambridge, UK)
• Jorge A. Pérez (University of Groningen, Netherlands)
• Ryosuke Sato (Tokyo University of Agriculture and Technology, Japan)
• Ilya Sergey (National University of Singapore, Singapore)
• Kathrin Stark (Heriot-Watt University, UK)
• Bernardo Toninho (NOVA FCT and NOVA LINCS, Portugal)
• Jana Wagemaker (Radboud University Nijmegen, Netherlands)
• John Wickerson (Imperial College London, UK)
• Fabio Zanasi (University College London, UK)

We welcome research papers submitted via a Journal-First channel at TOPLAS.

1. Authors submit their papers directly to TOPLAS before the Round 1 submission deadline, and in their cover letter indicate that they want their paper to be considered as an ESOP Journal-First paper.
2. Reviewing is handled exclusively by TOPLAS.
3. (Optionally, but highly recommended:) Authors notify the ESOP PC chair of their TOPLAS submission, so that the PC chair can follow up with the TOPLAS editor-in-chief about the status of these submissions.
4. If a TOPLAS Journal-First paper is accepted before the end of the Round 2 rebuttal period date, and the ESOP PC agrees, it may be presented at ETAPS.

Revised and expanded versions of accepted ESOP research papers are eligible for the ESOP Journal-After TOPLAS channel. A call will open in January after the ESOP notification. More details will be provided at a later moment.