Abstract is missing.
- What Makes a Mathematician Tick? (Invited Talk)Kevin Buzzard. [doi]
- Proving Tree Algorithms for Succinct Data StructuresReynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. [doi]
- Nine Chapters of Analytic Number Theory in Isabelle/HOLManuel Eberl. [doi]
- Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and DijkstraPeter Lammich, Tobias Nipkow. [doi]
- A Certificate-Based Approach to Formally Verified ApproximationsFlorent Bréhard, Assia Mahboubi, Damien Pous. [doi]
- A Verified LL(1) Parser GeneratorSam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux. [doi]
- Declarative Proof Translation (Short Paper)Cezary Kaliszyk, Karol Pak. [doi]
- A Formalization of Forcing and the Unprovability of the Continuum HypothesisJesse Michael Han, Floris van Doorn. [doi]
- Higher-Order Tarski Grothendieck as a Foundation for Formal ProofChad E. Brown, Cezary Kaliszyk, Karol Pak. [doi]
- Quantitative Continuity and Computable Analysis in CoqFlorian Steinberg, Laurent Théry, Holger Thies. [doi]
- Verified Decision Procedures for Modal LogicsMinchao Wu, Rajeev Goré. [doi]
- The DPRM Theorem in Isabelle (Short Paper)Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher. [doi]
- Formalizing Computability Theory via Partial Recursive FunctionsMario Carneiro. [doi]
- Ornaments for Proof Reuse in CoqTalia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman. [doi]
- Hammering Mizar by Learning Clause Guidance (Short Paper)Jan Jakubuv, Josef Urban. [doi]
- First-Order Guarded Coinduction in CoqLukasz Czajka 0001. [doi]
- A Million Lines of Proof About a Moving Target (Invited Talk)June Andronick. [doi]
- Data Types as Quotients of Polynomial FunctorsJeremy Avigad, Mario Carneiro, Simon Hudon. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda CalculusYannick Forster 0002, Fabian Kunze. [doi]
- Virtualization of HOL4 in IsabelleFabian Immler, Jonas Rädle, Makarius Wenzel. [doi]
- Binary-Compatible Verification of Filesystems with ACL2Mihir Parang Mehta, William R. Cook. [doi]
- Generating Verified LLVM from Isabelle/HOLPeter Lammich. [doi]
- Formal Proof and Analysis of an Incremental Cycle Detection AlgorithmArmaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier. [doi]
- Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOLMaximilian P. L. Haslbeck, Peter Lammich. [doi]
- An Increasing Need for Formality (Invited Talk)Martin Dixon. [doi]
- Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow SecurityRobert Sison, Toby Murray. [doi]
- Characteristic Formulae for Liveness Properties of Non-Terminating CakeML ProgramsJohannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen. [doi]
- Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in CoqEnrico Tassi. [doi]
- Formalizing the Solution to the Cap Set ProblemSander R. Dahmen, Johannes Hölzl, Robert Y. Lewis. [doi]
- Primitive Floats in CoqGuillaume Bertholon, Érik Martin-Dorel, Pierre Roux. [doi]
- Generic Authenticated Data Structures, FormallyMatthias Brun, Dmitriy Traytel. [doi]
- A Verified Compositional Algorithm for AI PlanningMohammad Abdulaziz, Charles Gretton, Michael Norrish. [doi]
- Formalization of the Domination Chain with Weighted Parameters (Short Paper)Daniel E. Severín. [doi]
- A Verified and Compositional Translation of LTL to Deterministic Rabin AutomataJulian Brunner 0001, Benedikt Seidl, Salomon Sickert. [doi]
- Complete Non-Orders and Fixed PointsAkihisa Yamada 0002, Jérémy Dubut. [doi]
- Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and IsabelleRan Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry. [doi]