default search action
Archive of Formal Proofs, Volume 2021
Volume 2021, 2021
- Susannah Mansky:
JinjaDCI: a Java semantics with dynamic class initialization. - Alejandro Gómez-Londoño:
Hood-Melville Queue. - Jakub Kadziolka:
Solution to the xkcd Blue Eyes puzzle. - Roland Coghetto:
Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid. - Manuel Eberl:
The Laws of Large Numbers. - Manuel Eberl:
Formal Puiseux Series. - Niels Mündler:
A Verified Imperative Implementation of B-Trees. - René Thiemann:
The Sunflower Lemma of Erdős and Rado. - Ben Blumson:
Mereology. - Mnacho Echenim:
Quantum projective measurements and the CHSH inequality. - Manuel Eberl:
The Hermite-Lindemann-Weierstraß Transcendence Theorem. - Ralph Bottesch, Jose Divasón, René Thiemann:
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation. - Andreas Lochbihler, S. Reza Sefidgar:
Constructive Cryptography in HOL: the Communication Modeling Aspect. - Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Grothendieck's Schemes in Algebraic Geometry. - Benedikt Nordhoff:
Information Flow Control via Dependency Tracking. - Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel:
Formalization of Timely Dataflow's Progress Tracking Protocol. - Sebastiaan J. C. Joosten:
Gale-Stewart Games. - Katherine Cordwell, Yong Kiam Tan, André Platzer:
The BKR Decision Procedure for Univariate Real Arithmetic. - Tobias Nipkow, Simon Roßkopf:
Isabelle's Metalogic: Formalization and Proof Checker. - Susannah Mansky:
Regression Test Selection. - Aaron Crighton:
Hensel's Lemma for the p-adic Integers. - Jakub Kadziolka:
Lifting the Exponent. - Stepan Holub, Martin Raska, Stepán Starosta:
Combinatorics on Words Basics. - Stepan Holub, Stepán Starosta:
Graph Lemma. - Stepan Holub, Stepán Starosta:
Lyndon words. - Pasquale Noce:
A Shorter Compiler Correctness Proof for Language IMP. - Asta Halkjær From:
Public Announcement Logic. - Mark Wassell:
MiniSail - A kernel language for the ISA specification language SAIL. - Katharina Kreuzer, Manuel Eberl:
Van der Waerden's Theorem. - Kevin Kappelmann, Lukas Bulwahn, Sebastian Willenbrink:
SpecCheck - Specification-Based Testing for Isabelle/ML. - Joseph Thommes, Manuel Eberl:
Finitely Generated Abelian Groups. - Walter Guttmann:
Relational Forests. - Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot:
Schutz' Independent Axioms for Minkowski Spacetime. - Chelsea Edmonds, Lawrence C. Paulson:
Combinatorial Design Theory. - Andrei Popescu, Thomas Bauereiss:
Fresh identifiers. - Fox Thomson, Wenda Li:
The Theorem of Three Circles. - Pasquale Noce:
Logging-independent Message Anonymity in the Relational Method. - René Thiemann:
Solving Cubic and Quartic Equations. - Nan Jiang:
A data flow analysis algorithm for computing dominators. - Mihails Milehins:
Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories. - Mihails Milehins:
Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories. - Mihails Milehins:
Category Theory for ZFC in HOL III: Universal Constructions. - Mihails Milehins:
Conditional Simplification. - Mihails Milehins:
Conditional Transfer Rule. - Mihails Milehins:
IDE: Introduction, Destruction, Elimination. - Mihails Milehins:
Extension of Types-To-Sets. - Christian Sternagel, René Thiemann, Akihisa Yamada:
A Formalization of Weighted Path Orders and Recursive Path Orders. - José Manuel Rodríguez Caballero, Dominique Unruh:
Complex Bounded Operators. - Asta Halkjær From:
Soundness and Completeness of an Axiomatic System for First-Order Logic. - Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer:
Verified Quadratic Virtual Substitution for Real Arithmetic. - Walter Guttmann:
Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations. - Freek Verbeek, Abhijith Bharadwaj, Joshua A. Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran:
X86 instruction semantics and basic block symbolic execution. - Valentin Fouillard, Safouan Taha, Frédéric Boulanger, Nicolas Sabouret:
Belief Revision Theory. - Dominique Unruh:
Quantum and Classical Registers. - Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Szemerédi's Regularity Lemma. - Manuel Eberl, René Thiemann:
Factorization of Polynomials with Algebraic Coefficients. - Christoph Benzmüller, Sebastian Reiche:
Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL. - Jacques D. Fleuriot:
Real Exponents as the Limits of Sequences of Rational Exponents. - Thomas Bauereiss, Andrei Popescu:
Compositional BD Security. - Andrei Popescu, Peter Lammich, Thomas Bauereiss:
CoCon: A Confidentiality-Verified Conference Management System. - Thomas Bauereiss, Andrei Popescu:
CoSMeDis: A confidentiality-verified distributed social media platform. - Thomas Bauereiss, Andrei Popescu:
CoSMed: A confidentiality-verified social media platform. - Christoph Benzmüller:
Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL. - Marie Cousin, Mnacho Echenim, Hervé Guiol:
The Hahn and Jordan Decomposition Theorems. - Fumiya Iwama:
Foundation of geometry in planes, and some complements: Excluding the parallel axioms. - Thomas Ammer, Peter Lammich:
van Emde Boas Trees. - Jesús Aransay, Alejandro del Campo, Julius Michaelis:
Simplicial Complexes and Boolean functions. - Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel:
Regular Tree Relations. - Maximilian Schäffeler, Mohammad Abdulaziz
:
Verified Algorithms for Solving Markov Decision Processes. - Maximilian Schäffeler, Mohammad Abdulaziz
Markov Decision Processes with Rewards. - Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson:
Roth's Theorem on Arithmetic Progressions. - Tobias Nipkow:
Gale-Shapley Algorithm. - Filip Smola, Jacques D. Fleuriot:
Hyperdual Numbers and Forward Differentiation.
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-12-23 19:19 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: