default search action
Archive of Formal Proofs, Volume 2020
Volume 2020, 2020
- Eugene W. Stark:
Bicategories. - Max W. Haslbeck, Manuel Eberl:
Skip Lists. - Martin Rau, Tobias Nipkow:
Closest Pair of Points Algorithms. - Robin Eßmann, Tobias Nipkow, Simon Robillard:
Verified Approximation Algorithms. - Manuel Eberl:
Mersenne primes and the Lucas-Lehmer test. - Walter Guttmann, Bernhard Möller:
A Hierarchy of Algebras for Boolean Subsets. - José Manuel Rodríguez Caballero:
Arithmetic progressions and relative primes. - Martin Desharnais:
A Generic Framework for Verified Compilers. - Bertram Felgenhauer:
Implementing the Goodstein Function in λ-Calculus. - Cornelius Diekmann, Lars Hupel:
Hello World. - Toby Murray:
An Under-Approximate Relational Logic. - Manuel Eberl:
Furstenberg's topology and his proof of the infinitude of primes. - Emin Karayel, Edgar Gonzàlez:
Strong Eventual Consistency of the Collaborative Editing Framework WOOT. - Chelsea Edmonds:
Lucas's Theorem. - Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel:
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations. - Sophie Tourret:
A Comprehensive Framework for Saturation Theorem Proving. - Lukas Heimes, Dmitriy Traytel, Joshua Schneider:
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows. - Andreas Lochbihler, Ognjen Maric:
Authenticated Data Structures As Functors. - Manuel Eberl:
Gaussian Integers. - Manuel Eberl:
The Lambert W Function on the Reals. - Manuel Eberl:
Power Sum Polynomials. - Florian Kammueller:
Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems. - Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, Anders Schlichtkrull:
Automated Stateful Protocol Verification. - Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker:
Stateful Protocol Composition and Typing. - Jonathan Julián Huerta y Munive:
Matrices for ODEs. - Dominique Unruh, José Manuel Rodríguez Caballero:
Banach-Steinhaus Theorem. - Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf:
Formalization of Forcing in Isabelle/ZF. - Salomon Sickert:
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation. - Georgy Dunaev:
Recursion Theorem in ZF. - Angeliki Koutsoukou-Argyraki, Wenda Li:
Irrationality Criteria for Series by Erdős and Straus. - Christian Sternagel, René Thiemann:
A Formalization of Knuth-Bendix Orders. - Lawrence C. Paulson:
The Nash-Williams Partition Theorem. - Jose Divasón:
A verified algorithm for computing the Smith normal form of a matrix. - Albert Rizaldi, Fabian Immler:
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles. - Walter Guttmann, Peter Höfner:
Relational Characterisations of Paths. - Ben Fiedler, Dmitriy Traytel:
A Formal Proof of The Chandy-Lamport Distributed Snapshot Algorithm. - Lawrence C. Paulson:
Ordinal Partitions. - Angeliki Koutsoukou-Argyraki:
Amicable Numbers. - Peter Gammie:
Putting the 'K' into Bird's derivation of Knuth-Morris-Pratt string matching. - Walter Guttmann:
Relational Disjoint-Set Forests. - Frank J. Balbach:
Some classical results in inductive inference of recursive functions. - Mathias Fleury, Daniela Kaufmann:
Practical Algebraic Calculus Checker. - Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick:
Inference of Extended Finite State Machines. - Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick:
A Formal Model of Extended Finite State Machines. - Andrei Popescu, Dmitriy Traytel:
From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. - Andrei Popescu, Dmitriy Traytel:
From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. - Andrei Popescu, Dmitriy Traytel:
An Abstract Formalization of Gödel's Incompleteness Theorems. - Andrei Popescu, Dmitriy Traytel:
Robinson Arithmetic. - Andrei Popescu, Dmitriy Traytel:
Syntax-Independent Logic Infrastructure. - Simon Foster, Burkhart Wolff:
A Sound Type System for Physical Quantities, Units, and Measurements. - Mohammad Abdulaziz, Peter Lammich:
AI Planning Languages Semantics. - Mohammad Abdulaziz, Friedrich Kurz:
Verified SAT-Based AI Planning. - Achim D. Brucker, Michael Herzberg:
The Safely Composable DOM. - Achim D. Brucker, Michael Herzberg:
A Formalization of Safely Composable Web Components. - Achim D. Brucker, Michael Herzberg:
A Formal Model of the Safely Composable Document Object Model with Shadow Roots. - Javier Díaz:
Finite Map Extras. - Anthony Bordg, Hanna Lachnitt, Yijun He:
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information. - Pasquale Noce:
The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols. - Walter Guttmann, Nicolas Robinson-O'Brien:
Relational Minimum Spanning Tree Algorithms. - David Fuenmayor:
Topological semantics for paraconsistent and paracomplete logics. - Pedro Sánchez Terraf:
Cofinality and the Delta System Lemma. - Safouan Taha, Burkhart Wolff, Lina Ye:
The HOL-CSP Refinement Toolkit. - Jasmin Blanchette, Sophie Tourret:
Extensions to the Comprehensive Framework for Saturation Theorem Proving. - Achim D. Brucker, Michael Herzberg:
A Formalization of Web Components. - Achim D. Brucker, Michael Herzberg:
A Formal Model of the Document Object Model with Shadow Roots. - Martin Desharnais:
Inline Caching and Unboxing Optimization for Interpreters.
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-18 20:33 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: