Abstract is missing.
- Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la FittingAsta Halkjær From, Anders Schlichtkrull. [doi]
- An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue SystemsDohan Kim 0001. [doi]
- Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOLJan van Brügge, Andrei Popescu 0001, Dmitriy Traytel. [doi]
- Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOLHanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds 0001, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli. [doi]
- Scott's Representation Theorem and the Univalent Karoubi EnvelopeArnoud van der Leer, Kobe Wullaert, Benedikt Ahrens. [doi]
- Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley GroupsEric Wang, Arohee Bhoja, Cayden R. Codel, Noah G. Singer. [doi]
- Formalizing Splitting in Isabelle/HOLGhilain Bergeron, Florent Krasnopol, Sophie Tourret. [doi]
- A Formal Analysis of Algorithms for Matroids and GreedoidsMohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa. [doi]
- A Mechanized First-Order Theory of Algebraic Data Types with Pattern MatchingJoshua M. Cohen. [doi]
- A Verified Cost Model for Call-By-Push-ValueZhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah. [doi]
- Verifying Datalog Reasoning with LeanJohannes Tantow, Lukas Gerlach 0002, Stephan Mennicke, Markus Krötzsch. [doi]
- On Verifying Secret Control Flow EliminationDavid Knothe, Oliver Bringmann 0001. [doi]
- Sledgehammering Without ATPs (Short Paper)Martin Desharnais, Jasmin Blanchette. [doi]
- A Formalization of Divided Powers in LeanAntoine Chambert-Loir, María Inés de Frutos-Fernández. [doi]
- Formalizing Concentration Inequalities in Rocq: Infrastructure and AutomationReynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux 0001, Takafumi Saikawa. [doi]
- Formalizing the Hidden Number Problem in Isabelle/HOLSage Binder, Eric Ren, Katherine Kosaian. [doi]
- Mechanising Böhm Trees and λη-CompletenessChun Tian 0001, Michael Norrish. [doi]
- Nondeterministic Asynchronous Dataflow in Isabelle/HOLRafael Castro Gonçalves Silva, Laouen Fernet, Dmitriy Traytel. [doi]
- Verification of the CVM Algorithm with a Functional Probabilistic InvariantEmin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan. [doi]
- Finiteness of Symbolic Derivatives in LeanEkaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner. [doi]
- Automatically Generalizing Proofs and StatementsAnshula Gandhi, Anand Rao Tadipatri, Timothy Gowers. [doi]
- A Formal Proof of Complexity Bounds on Diophantine EquationsJonas Bayer, Marco David. [doi]
- Taming Floating-Point Rounding Errors with Proofs (Invited Talk)Laura Titolo. [doi]
- A Certified Proof Checker for Deep Neural Network Verification in ImandraRemi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, Guy Katz. [doi]
- LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)Eric Vin, Kyle A. Miller, Daniel J. Fremont. [doi]
- A Natural Language Formalization of Perfectoid Rings in ℕaprochePeter Koepke. [doi]
- Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation ProofsJérémy Thibault, Joseph Lenormand, Catalin Hritcu. [doi]
- Inductive Predicates via Least Fixpoints in Higher-Order Separation LogicRobbert Krebbers, Luko van der Maas, Enrico Tassi. [doi]
- Formalising New Mathematics in Isabelle: Diagonal RamseyLawrence C. Paulson. [doi]
- Formally Verifying a Vertical Cell Decomposition AlgorithmYves Bertot, Thomas Portet. [doi]
- Barendregt's Theory of the λ-Calculus, Refreshed and FormalizedAdrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Formalising Subject Reduction and Progress for Multiparty Session ProcessesBurak Ekici, Tadayoshi Kamegai, Nobuko Yoshida. [doi]
- Formalising Inductive and Coinductive ContainersStefania Damato, Thorsten Altenkirch, Axel Ljungström. [doi]
- Certified Implementability of Global Multiparty ProtocolsElaine Li, Thomas Wies. [doi]
- Program Optimisations via Hylomorphisms for Extraction of Executable CodeDavid Castro-Perez, Marco Paviotti, Michael Vollmer 0003. [doi]
- Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk)Kathrin Stark. [doi]
- Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper)Nadeem Abdul Hamid. [doi]
- Canonical for Automated Theorem Proving in LeanChase Norman, Jeremy Avigad. [doi]
- Verifying an Efficient Algorithm for Computing Bernoulli NumbersManuel Eberl, Peter Lammich. [doi]
- GOL in GOL in HOL: Verified Circuits in Conway's Game of LifeMagnus O. Myreen, Mario Carneiro. [doi]