default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDArchive of Formal Proofs, Volume 2023
Volume 2023, 2023
- Stepan Holub, Martin Raska:
Binary codes that do not preserve primitivity. - Stepan Holub, Stepán Starosta:
Intersection of two monoids generated by two element codes. - Frank J. Balbach:
The Cook-Levin theorem. - Asta Halkjær From:
Synthetic Completeness. - Anthony Bordg, Adrián Doña Mateo:
Strict Omega Categories. - Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka:
A Hoare Logic for Diverging Programs. - Matthew Doty:
Suppes' Theorem For Probability Logic. - Jasmin Christian Blanchette, Qi Qiu, Sophie Tourret:
Given Clause Loops. - Shuwei Hu:
ABY3 Multiplication and Array Shuffling. - Katharina Kreuzer:
Hardness of Lattice Problems. - Rodrigo Raya:
Group Law of Edwards Elliptic Curves. - Matthew Doty:
A Sound and Complete Calculus for Probability Inequalities. - Andrei Popescu:
Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion. - Emin Karayel:
Expander Graphs. - Mike Stannett, Edward Higgins, Hajnal Andréka, Judit X. Madarász, István Németi, Gergely Székely:
No Faster-Than-Light Observers (GenRel). - Thibault Dardinier:
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs. - Emin Karayel:
Distributed Distinct Elements. - Thibault Dardinier:
Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. - Charles Staats:
Positional Notation for Natural Numbers in an Arbitrary Base. - Martin Desharnais:
A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic. - Sunpill Kim, Yong Kiam Tan:
The Schwartz-Zippel Lemma. - Mike Stannett:
The Halting Problem is Soluble in Malament-Hogarth Spacetimes. - Mnacho Echenim, Mehdi Mhalla, Coraline Mori:
The CHSH inequality: Tsirelson's upper-bound and other results. - Anton Danilkin, Loïc Chevalier:
Three Squares Theorem. - Lukas Stevens:
MLSS Decision Procedure. - Nils Cremer:
Tree Enumeration. - Walter Guttmann, Georg Struth:
Inner Structure, Determinism and Modal Algebra of Multirelations. - René Thiemann, Elias Wenninger:
A Verified Efficient Implementation of the Weighted Path Order. - A. Whitley:
Cryptographic Standards. - Christian Dalvit:
Zeckendorf's Theorem. - Axel Kjeld Fjelrad Christfort, Søren Debois:
DCR Syntax and Execution Equivalent Markings. - Emin Karayel, Manuel Eberl:
Executable Randomized Algorithms. - Maximilian Spitz:
Gray Codes for Arbitrary Numeral Systems. - Martin Rau:
Earley Parser. - Georg Struth, Cameron Calk:
Modal quantales, involutive quantales, Dedekind Quantales. - Kevin Lee, Zhengkun Ye, Angeliki Koutsoukou-Argyraki:
Polygonal Number Theorem. - Akihisa Yamada, Jérémy Dubut:
Formalizing Results on Directed Sets. - Georg Struth:
Catoids, Categories, Groupoids. - Lars Hupel:
Fixed-length vectors. - Mathias Schack Rabing:
Ceva's Theorem. - Michikazu Hirata, Yasuhiko Minamide:
S-Finite Measure Monad on Quasi-Borel Spaces. - Michikazu Hirata:
Standard Borel Spaces. - Benjamin Bisping, Luisa Montanari:
Coupled Similarity and Contrasimilarity, and How to Compute Them. - Robert Sachtleben:
Conformance Relations between Input/Output Languages. - Lawrence C. Paulson:
Euler's Polyhedron Formula. - Kevin Kappelmann:
Unification Utilities for Isabelle/ML. - Chelsea Edmonds:
General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma. - Chelsea Edmonds:
Hypergraphs. - Walter Guttmann:
Cardinality and Representation of Stone Relation Algebras. - Chelsea Edmonds, Lawrence C. Paulson:
Hypergraph Colouring Bounds. - Ata Keskin:
Eudoxus Reals. - Katharina Kreuzer, Manuel Eberl:
Elimination of Repeated Factors Algorithm. - Manuel Eberl, Katharina Kreuzer:
Perfect Fields. - Kevin Kappelmann:
Transport via Partial Galois Connections and Equivalences. - Michikazu Hirata:
Disintegration Theorem. - Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel:
Labeled Transition Systems. - Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel:
Pushdown Systems. - Javier Díaz:
Metatheory of Q0. - Cárolos Laméris:
Myhill-Nerode Theorem for Nominal G-Automata. - Manuel Eberl:
Chebyshev Polynomials. - Emin Karayel, Yong Kiam Tan:
Concentration Inequalities. - Manuel Eberl:
Two theorems about the geometry of the critical points of a complex polynomial. - Manuel Eberl:
The Cardinality of the Continuum. - Manuel Eberl:
The Polylogarithm Function. - Anders Schlichtkrull:
Soundness of the Q0 proof system for higher-order logic. - Ata Keskin:
Martingales. - Manuel Eberl:
Lambert Series. - Lawrence C. Paulson:
Knuth-Morris-Pratt String Search. - Benoît Ballenghien, Safouan Taha, Burkhart Wolff:
HOL-CSPM - Architectural operators for HOL-CSP. - Katharina Kreuzer:
CRYSTALS-Kyber_Security. - Benoît Ballenghien, Burkhart Wolff:
Operational Semantics formally proven in HOL-CSP.
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 2025-11-22 00:31 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:
