ESOP 2025

32 papers

1. A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming · Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, Fabio Zanasi
2. A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model · Weijie Fan, Hongjin Liang, Xinyu Feng, Hanru Jiang
3. Abstraction of memory block manipulations by symbolic loop folding · Jérôme Boillot, Jérôme Feret
4. An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols · Felix Stutz, Emanuele D'Osualdo
5. An abstract, certified account of operational game semantics · Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski
6. Artifact Report: an Abstract, Certified Account of Operational Game Semantics · Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski
7. CUTECat: Concolic Execution for Computational Law · Pierre Goutagny, Aymeric Fromherz, Raphaël Monat
8. Cognacy Queries over Dependence Graphs for Transparent Visualisations · Joseph Bond, Cristina David, Minh Nguyen, Dominic Orchard, Roly Perera
9. Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration · Florian Sextl, Adam Rogalewicz, Tomás Vojnar, Florian Zuleger
10. Constructive characterisations of the MUST-preorder for asynchrony · Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, Léo Stefanesco
11. Context-Dependent Effects in Guarded Interaction Trees · Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal
12. Context-Sensitive Demand-Driven Control-Flow Analysis · Tim Whiting, Kimball Germane
13. Coverage Semantics for Dependent Pattern Matching · Joseph Eremondi, Ohad Kammar
14. Efficient Synthesis of Tight Polynomial Upper-Bounds for Systems of Conditional Polynomial Recurrences · Amir Kafshdar Goharshady, S. Hitarth, Sergei Novozhilov
15. Elucidating Type Conversions in SQL Engines · Wenjia Ye, Matías Toro, Claudio Gutierrez, Bruno C. d. S. Oliveira, Éric Tanter
16. First-Person Choreographic Programming with Continuation-Passing Communications · Sung-Shik Jongmans
17. Formal Autograding in a Classroom · Dragana Milovancevic, Mario Bucev, Marcin Wojnarowski, Samuel Chassot, Viktor Kuncak
18. Formal Verification of WTO-based Dataflow Solvers · Roméo La Spina, Delphine Demange, Sandrine Blazy
19. Formal Verification of WTO-based Dataflow Solvers - Artifact Experience Report · Roméo La Spina, Delphine Demange, Sandrine Blazy
20. Formulas as Processes, Deadlock-Freedom as Choreographies · Matteo Acclavio, Giulia Manara, Fabrizio Montesi
21. Iso-Recursive Multiparty Sessions and their Automated Verification · Marco Giunti, Nobuko Yoshida
22. Multiparty Session Types with a Bang! · Matthew Alan Le Brun, Simon Fowler, Ornela Dardha
23. Named Arguments as Intersections, Optional Arguments as Unions · Yaozhu Sun, Bruno C. d. S. Oliveira
24. Neural Network Verification is a Programming Language Challenge · Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T. Johnson, Guy Katz + 5 more
25. On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic · Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
26. SMT-Boosted Security Types for Low-Level MPC · Christian Skalka, Joseph P. Near
27. Stratified Type Theory · Jonathan Chan, Stephanie Weirich
28. Sufficient Conditions for Robustness of RDMA Programs · Guillaume Ambal, Ori Lahav, Azalea Raad
29. The Vanilla Sequent Calculus is Call-by-Value · Beniamino Accattoli
30. Variable Elimination as Rewriting in a Linear Lambda Calculus · Thomas Ehrhard, Claudia Faggian, Michele Pagani
31. Verifying Algorithmic Versions of the Lovász Local Lemma · Rongen Lin, Hongjin Liang, Xinyu Feng
32. coma, an Intermediate Verification Language with Explicit Abstraction Barriers · Andrei Paskevich, Paul Patault, Jean-Christophe Filliâtre