Abstract is missing.
- CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)Sandrine Blazy. 1 [doi]
- Improved Assistance for Interactive Proof (Keynote)Cezary Kaliszyk. 2 [doi]
- Semantics of Probabilistic Programs using s-Finite Kernels in CoqReynald Affeldt, Cyril Cohen, Ayumu Saito. 3-16 [doi]
- A Formal Disproof of Hirsch ConjectureXavier Allamigeon, Quentin Canu, Pierre-Yves Strub. 17-29 [doi]
- FastVer2: A Provably Correct Monitor for Concurrent, Key-Value StoresArvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy. 30-46 [doi]
- Formalized Class Group Computations and Integral Points on Mordell Elliptic CurvesAnne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen. 47-62 [doi]
- Compositional Pre-processing for Automated Reasoning in Dependent Type TheoryValentin Blot, Denis Cousineau 0003, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial. 63-77 [doi]
- Encoding Dependently-Typed Constructions into Simple Type TheoryAnthony Bordg, Adrián Doña Mateo. 78-89 [doi]
- A Formalized Reduction of Keller's ConjectureJoshua Clune. 90-101 [doi]
- Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection ConstructivelyMatthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi. 102-120 [doi]
- Formalising the h-Principle and Sphere EversionFloris van Doorn, Patrick Massot, Oliver Nash. 121-134 [doi]
- Terms for Efficient Proof Checking and ParsingMichael Färber 0002. 135-147 [doi]
- Formalizing and Computing Propositional QuantifiersHugo Férée, Sam van Gool. 148-158 [doi]
- A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl)Yannick Forster 0002, Felix Jahn, Gert Smolka. 159-166 [doi]
- Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-ElpiBenjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. 167-181 [doi]
- Mechanised Semantics for Gated Static Single AssignmentYann Herklotz, Delphine Demange, Sandrine Blazy. 182-196 [doi]
- A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite SystemsChristina Kohl, Aart Middeldorp. 197-210 [doi]
- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOLKatherine Kosaian, Yong Kiam Tan, André Platzer. 211-224 [doi]
- A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOLAngeliki Koutsoukou Argyraki, Mantas Baksys, Chelsea Edmonds. 225-238 [doi]
- Computing Cohomology Rings in Cubical AgdaThomas Lamiaux, Axel Ljungström, Anders Mörtberg. 239-252 [doi]
- Aesop: White-Box Best-First Proof Search for LeanJannis Limperg, Asta Halkjær From. 253-266 [doi]
- Formalising Sharkovsky's Theorem (Proof Pearl)Bhavik Mehta. 267-274 [doi]
- ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DERHaobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy. 275-289 [doi]
- Formalising Decentralised Exchanges in CoqEske Hoy Nielsen, Danil Annenkov, Bas Spitters. 290-302 [doi]
- P4Cub: A Little Language for Big RoutersRudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster. 303-319 [doi]
- Verifying Term Graph Optimizations using Isabelle/HOLBrae J. Webb, Ian J. Hayes, Mark Utting. 320-333 [doi]
- A Formalization of Doob's Martingale Convergence Theorems in mathlibKexing Ying, Rémy Degenne. 334-347 [doi]