Formalization of the Domination Chain with Weighted Parameters (short paper)
Nine Chapters of Analytic Number Theory in Isabelle/HOL
Binary-compatible verification of filesystems with ACL2
Ornaments for Proof Reuse in Coq
Verifying that a compiler preserves concurrent value-dependent information-flow security
Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
Refinement with Time — Refining the Run-time of Algorithms in Isabelle/HOL
Higher-order Tarski Grothendieck as a Foundation for Formal Proof
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
A certifying extraction with time bounds from Coq to call-by-value λ-calculus
Generating Verified LLVM from Isabelle/HOL
Declarative Proof Translation (short paper)
Complete Non-Orders and Fixed Points
Generic Authenticated Data Structures, Formally
Formal Proof of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq, and Isabelle
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra
Data types as quotients of polynomial functors
A Verified Compositional Algorithm for AI Planning
Formalizing computability theory via partial recursive functions
Verified Decision Procedures for Modal Logics
Formalizing the Solution to the Cap Set Problem
Quantitative continuity and computable analysis in Coq
Hammering Mizar by Learning Clause Guidance (short paper)
First-order guarded coinduction in Coq
Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs
The DPRM theorem in Isabelle (short paper)
A certificate-based approach to formally verified approximations
Proving tree algorithms for succinct data structures
A Verified LL(1) Parser Generator
Virtualization of HOL4 in Isabelle
A formalization of forcing and the consistency of the failure of the continuum hypothesis
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
Primitive Floats in Coq