| 2024 | Hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions. | Michael Hanus |
| 2024 | Non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures. | Vtor Fernandes, Marc de Visme, Benot Valiron |
| 2024 | A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution. | Thi Thu Ha Doan, Peter Thiemann |
| 2024 | Quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers. | Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, Gabriele Tedeschi |
| 2024 | Extending the Quantitative Pattern-Matching Paradigm. | Sandra Alves, Delia Kesner, Miguel Ramos |
| 2024 | Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. | Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North |
| 2023 | Towards a Framework for Developing Verified Assemblers for the ELF Format. | Jinhua Wu, Yuting Wang, Meng Sun, Xiangzhe Xu, Yichen Song |
| 2023 | Proofs as Terms, Terms as Graphs. | Jui-Hsuan Wu |
| 2023 | Compilation Semantics for a Programming Language with Versions. | Yudai Tanabe, Luthfan Anshar Lubis, Tomoyuki Aotani, Hidehiko Masuhara |
| 2023 | What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical Study. | Ke Sun, Sheng Chen, Meng Wang, Dan Hao |
| 2023 | TorchProbe: Fuzzing Dynamic Deep Learning Compilers. | Qidong Su, Chuqin Geng, Gennady Pekhimenko, Xujie Si |
| 2023 | Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq. | Ayumu Saito, Reynald Affeldt |
| 2023 | Types and Semantics for Extensible Data Types. | Cas van der Rest, Casper Bach Poulsen |
| 2023 | Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection. | Wenhua Li, Quang Loc Le, Yahui Song, Wei-Ngan Chin |
| 2023 | A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists. | Clemens Kupke, Fredrik Nordvall Forsberg, Sean Watters |
| 2023 | Transport via Partial Galois Connections and Equivalences. | Kevin Kappelmann |
| 2023 | Argument Reduction of Constrained Horn Clauses Using Equality Constraints. | Ryo Ikeda, Ryosuke Sato, Naoki Kobayashi |
| 2023 | Typed Non-determinism in Functional and Concurrent Calculi. | Bas van den Heuvel, Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Prez |
| 2023 | m-CFA Exhibits Perfect Stack Precision. | Kimball Germane |
| 2023 | Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. | Yannick Forster, Dominik Kirst, Niklas Mck |
| 2023 | A Diamond Machine for Strong Evaluation. | Beniamino Accattoli, Pablo Barenbaum |
| 2022 | A Calculus with Recursive Types, Record Concatenation and Subtyping. | Yaoda Zhou, Bruno C. d. S. Oliveira, Andong Fan |
| 2022 | Applicative Intersection Types. | Xu Xue, Bruno C. d. S. Oliveira, Ningning Xie |
| 2022 | Automated Temporal Verification for Algebraic Effects. | Yahui Song, Darius Foo, Wei-Ngan Chin |
| 2022 | Inferring Region Types via an Abstract Notion of Environment Transformation. | Ulrich Schpp, Chuangjie Xu |