![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Archive of Formal Proofs, Volume 2024
Volume 2024, 2024
- Achim D. Brucker, Amy Stell:
(Extended) Interval Analysis. - Sebastián Buss:
Decomposition of totally ordered hoops. - Cameron Calk, Georg Struth:
Higher Globular Catoids and Quantales. - Tobias Nipkow:
Region Quadtrees. - Azucena Garvía Bosshard, Christoph Sprenger, Jonathan Bootle:
The Sumcheck Protocol. - Pasquale Noce:
Information Flow Control via Stateful Intransitive Noninterference in Language IMP. - Terru Stübinger, Lars Hupel:
Go Code Generation for Isabelle. - Georg Struth, Tanguy Massacrier:
Cubical Categories. - Jakob Schulz, Emin Karayel:
Karatsuba Multiplication on Integers. - Axel Bergström, Tjark Weber:
Verified QBF Solving. - Jamie Chen:
Wieferich-Kempner Theorem. - Ata Keskin:
Doob's Upcrossing Inequality and Martingale Convergence Theorem. - Xavier Parent, Christoph Benzmüller:
Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). - Yong Kiam Tan, Jiong Yang:
Approximate Model Counting. - Manuel Eberl:
Continued Fractions. - Manuel Eberl:
Kummer's congruence. - Alexander Treml:
Uncertainty Principle. - Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber:
Broadcast Psi-calculi. - Peter Gammie:
ConcurrentHOL. - Emin Karayel:
Derandomization with Conditional Expectations. - Andrei Herasimau, Jonathan Julián Huerta y Munive, Leonardo Lima, Martin Raszyk, Dmitriy Traytel:
A Verified Proof Checker for Metric First-Order Temporal Logic. - Vincent Trélat:
Substitutions for Lambda-Free Higher-Order Terms. - René Thiemann, Fabian Mitterwallner, Aart Middeldorp:
Undecidability Results on Orienting Single Rewrite Rules. - Achim D. Brucker, Nicolas Méric, Burkhart Wolff:
Isabelle/DOF. - Sage Binder, Katherine Kosaian:
Pick's Theorem. - Sarah Tilscher, Simon Wimmer:
LL(1) Parser Generator. - Shuhao Song, Bowen Yao:
Prime Number Theorem with Remainder Term. - Yannick Stade, Sarah Tilscher, Helmut Seidl:
Partial Correctness of the Top-Down Solver. - Jakob Schulz:
Schönhage-Strassen Multiplication.
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
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.