| 2024 | "Repressed book: (re)presentation of National Cultural Heritage from the Funds of the Vasyl Stefanyk National Scientific Library of Ukraine in Lviv" - Information Technologies for the Implementation of a Cross-Sectoral Project. | Galyna Melnyk-Khokha, Nadiia Popadiuk, Nadiia Zubko, Valentyna Mudrokha |
| 2024 | Digitalization of HR management in government agencies. | Hrystyna Matkivska, Oleg Zachko |
| 2024 | Teaching Mathematics Using Lean and Controlled Natural Language. | Patrick Massot |
| 2024 | A Formalization of the General Theory of Quaternions. | Thaynara Arielly de Lima, Andr Luiz Galdino, Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincn |
| 2024 | The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. | Yann Leray, Gatan Gilbert, Nicolas Tabareau, Tho Winterhalter |
| 2024 | The project formation of virtual graphic images in applications for distance education systems. | Vitaliy Lazoryshynets, Volodymyr Pasichnyk, Nataliia Kunanets, Olga Artemenko, Andrii Sihaiov, Hanna Hesheva |
| 2024 | Formalizing the Cholesky Factorization Theorem. | Carl Kwan, Warren A. Hunt Jr. |
| 2024 | Supply chain management information system project with the use of digital twins. | Nataliia Kunanets, Kateryna Semenchuk, Liubava S. Chernova |
| 2024 | A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. | Vincent Jackson, Toby Murray, Christine Rizkallah |
| 2024 | Distributed Parallel Build for the Isabelle Archive of Formal Proofs. | Fabian Huch, Makarius Wenzel |
| 2024 | A Formalization of the Lvy-Prokhorov Metric in Isabelle/HOL. | Michikazu Hirata |
| 2024 | Formalizing the Algebraic Small Object Argument in UniMath. | Dennis Hilhorst, Paige Randall North |
| 2024 | Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. | Marc Hermes, Robbert Krebbers |
| 2024 | Mechanized HOL Reasoning in Set Theory. | Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak |
| 2024 | Verifying Software Emulation of an Unsupported Hardware Instruction. | Samuel Gruetter, Thomas Bourgeat, Adam Chlipala |
| 2024 | A Formal Proof of R(4, 5)=25. | Thibault Gauthier, Chad E. Brown |
| 2024 | Typed Compositional Quantum Computation with Lenses. | Jacques Garrigue, Takafumi Saikawa |
| 2024 | End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. | Florian Faissole, Paul Geneau de Lamarlire, Guillaume Melquiond |
| 2024 | Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). | Sam Ezeh |
| 2024 | Completeness of Asynchronous Session Tree Subtyping in Coq. | Burak Ekici, Nobuko Yoshida |
| 2024 | Formalising Half of a Graduate Textbook on Number Theory (Short Paper). | Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li |
| 2024 | Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. | Floris van Doorn, Heather Macbeth |
| 2024 | Enhancing Urban Planning with LoRa and GANs: A Project Management Perspective. | Serhii Dolhopolov, Tetyana Honcharenko, Illia Sachenko, Denys Gergi |
| 2024 | A Modular Formalization of Superposition in Isabelle/HOL. | Martin Desharnais, Balzs Tth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret |
| 2024 | Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. | Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad |