Accepted Papers





Daniel Severin. Formalization of the Domination Chain with Weighted Parameters (short paper)
Manuel Eberl. Nine Chapters of Analytic Number Theory in Isabelle/HOL
Mihir Mehta and William Cook. Binary-compatible verification of filesystems with ACL2
Talia Ringer, Nathaniel Yazdani, John Leo and Dan Grossman. Ornaments for Proof Reuse in Coq
Robert Sison and Toby Murray. Verifying that a compiler preserves concurrent value-dependent information-flow security
Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
Maximilian Paul Louis Haslbeck and Peter Lammich. Refinement with Time — Refining the Run-time of Algorithms in Isabelle/HOL
Chad Brown, Cezary Kaliszyk and Karol Pąk. Higher-order Tarski Grothendieck as a Foundation for Formal Proof
Salomon Sickert, Julian Brunner and Benedikt Seidl. A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
Yannick Forster and Fabian Kunze. A certifying extraction with time bounds from Coq to call-by-value λ-calculus
Peter Lammich. Generating Verified LLVM from Isabelle/HOL
Cezary Kaliszyk and Karol Pąk. Declarative Proof Translation (short paper)
Akihisa Yamada and Jérémy Dubut. Complete Non-Orders and Fixed Points
Matthias Brun and Dmitriy Traytel. Generic Authenticated Data Structures, Formally
Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz and Laurent Théry. Formal Proof of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq, and Isabelle
Peter Lammich and Tobias Nipkow. Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra
Jeremy Avigad, Mario Carneiro and Simon Hudon. Data types as quotients of polynomial functors
Mohammad Abdulaziz, Charles Gretton and Michael Norrish. A Verified Compositional Algorithm for AI Planning
Mario Carneiro. Formalizing computability theory via partial recursive functions
Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics
Sander Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem
Florian Steinberg, Laurent Thery and Holger Thies. Quantitative continuity and computable analysis in Coq
Jan Jakubuv and Josef Urban. Hammering Mizar by Learning Clause Guidance (short paper)
Łukasz Czajka. First-order guarded coinduction in Coq
Johannes Åman Pohjola, Henrik Rostedt and Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs
Marco David, Jonas Bayer, Abhik Pal and Benedikt Stock. The DPRM theorem in Isabelle (short paper)
Florent Bréhard, Assia Mahboubi and Damien Pous. A certificate-based approach to formally verified approximations
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi and Kazunari Tanaka. Proving tree algorithms for succinct data structures
Sam Lasser, Chris Casinghino, Kathleen Fisher and Cody Roux. A Verified LL(1) Parser Generator
Fabian Immler, Jonas Rädle and Makarius Wenzel. Virtualization of HOL4 in Isabelle
Jesse Han and Floris van Doorn. A formalization of forcing and the consistency of the failure of the continuum hypothesis
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
Guillaume Bertholon, Érik Martin-Dorel and Pierre Roux. Primitive Floats in Coq


Comments are closed.