| 2026 | Linear Effects, Exceptions, and Resource Safety - A Curry-Howard Correspondence for Destructors. | Sidney Congard, Guillaume Munch-Maccagnoni, Rmi Douence |
| 2026 | Code Generation via Meta-programming in Dependently Typed Proof Assistants. | Mathis Bouverot-Dupuis, Yannick Forster |
| 2026 | Recursive Logical Relations for Intuitionistic Linear Logic Session Types. | Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao |
| 2026 | Deciding not to Decide - Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism. | Patrycja Balik, Szymon Jedras, Piotr Polesiuk |
| 2026 | In Cantor Space No One Can Hear You Stream. | Martin Baillon, Assia Mahboubi, Pierre-Marie Pdrot |
| 2026 | Contextual Metaprogramming for Session Types. | Pedro ngelo, Atsushi Igarashi, Yuito Murase, Vasco T. Vasconcelos |
| 2026 | Specifying and Verifying RDMA Synchronisation. | Guillaume Ambal, Max Stupple, Brijesh Dongol, Azalea Raad |
| 2025 | Elucidating Type Conversions in SQL Engines. | Wenjia Ye, Matas Toro, Claudio Gutierrez, Bruno C. d. S. Oliveira, ric Tanter |
| 2025 | On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic. | Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato |
| 2025 | Context-Sensitive Demand-Driven Control-Flow Analysis. | Tim Whiting, Kimball Germane |
| 2025 | Named Arguments as Intersections, Optional Arguments as Unions. | Yaozhu Sun, Bruno C. d. S. Oliveira |
| 2025 | An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols. | Felix Stutz, Emanuele D'Osualdo |
| 2025 | Context-Dependent Effects in Guarded Interaction Trees. | Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal |
| 2025 | Formal Verification of WTO-based Dataflow Solvers - Artifact Experience Report. | Romo La Spina, Delphine Demange, Sandrine Blazy |
| 2025 | Formal Verification of WTO-based Dataflow Solvers. | Romo La Spina, Delphine Demange, Sandrine Blazy |
| 2025 | SMT-Boosted Security Types for Low-Level MPC. | Christian Skalka, Joseph P. Near |
| 2025 | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. | Florian Sextl, Adam Rogalewicz, Toms Vojnar, Florian Zuleger |
| 2025 | A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming. | Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, Fabio Zanasi |
| 2025 | coma, an Intermediate Verification Language with Explicit Abstraction Barriers. | Andrei Paskevich, Paul Patault, Jean-Christophe Fillitre |
| 2025 | Formal Autograding in a Classroom. | Dragana Milovancevic, Mario Bucev, Marcin Wojnarowski, Samuel Chassot, Viktor Kuncak |
| 2025 | Verifying Algorithmic Versions of the Lovsz Local Lemma. | Rongen Lin, Hongjin Liang, Xinyu Feng |
| 2025 | First-Person Choreographic Programming with Continuation-Passing Communications. | Sung-Shik Jongmans |
| 2025 | CUTECat: Concolic Execution for Computational Law. | Pierre Goutagny, Aymeric Fromherz, Raphal Monat |
| 2025 | Efficient Synthesis of Tight Polynomial Upper-Bounds for Systems of Conditional Polynomial Recurrences. | Amir Kafshdar Goharshady, S. Hitarth, Sergei Novozhilov |
| 2025 | Iso-Recursive Multiparty Sessions and their Automated Verification. | Marco Giunti, Nobuko Yoshida |