default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDArchive of Formal Proofs, Volume 2018
Volume 2018, 2018
- Christoph Traut, Fabian Immler:
Taylor Models. - Mohammad Abdulaziz
, Lawrence C. Paulson:
An Isabelle/HOL formalisation of Green's Theorem. - Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. - Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified LLL algorithm. - Christian Sternagel, René Thiemann:
First-Order Terms. - Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified factorization algorithm for integer polynomials with polynomial complexity. - Max W. Haslbeck, Manuel Eberl, Tobias Nipkow:
Treaps. - Manuel Eberl:
The Error Function. - Maximilian P. L. Haslbeck, Tobias Nipkow:
Hoare Logics for Time Bounds. - Diego Marmsoler:
A Theory of Architectural Design Patterns. - Tobias Nipkow, Stefan Dirix:
Weight-Balanced Trees. - Felix Brandt, Manuel Eberl, Christian Saile, Christian Stricker:
The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency. - Andreas Lochbihler, Joshua Schneider:
Bounded Natural Functors with Covariance and Contravariance. - Peter Lammich, Simon Wimmer:
VerifyThis 2018 - Polished Isabelle Solutions. - Conrad Watt:
WebAssembly. - Oliver Bracevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock, Markus Tasch:
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties. - Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan, Alastair R. Beresford:
OpSets: Sequential Specifications for Replicated Datatypes. - Simon Wimmer, Shuwei Hu, Tobias Nipkow:
Monadification, Memoization and Dynamic Programming. - Christoph Benzmüller, Dana S. Scott:
Axiom Systems for Category Theory in Free Logic. - Angeliki Koutsoukou-Argyraki, Wenda Li:
Irrational Rapidly Convergent Series. - Simon Wimmer, Johannes Hölzl:
Probabilistic Timed Automata. - Simon Wimmer:
Hidden Markov Models. - Tobias Nipkow, Dániel Somogyi:
Optimal Binary Search Trees. - Anthony Bordg:
The Localization of a Commutative Ring. - Anthony Bordg:
Projective Geometry. - Sebastien Gouezel:
Gromov Hyperbolicity. - Lars Hupel:
CakeML. - Julian Brunner:
Partial Order Reduction. - Manuel Eberl:
Pell's Equation. - Julian Parsert, Cezary Kaliszyk:
Von-Neumann-Morgenstern Utility Theorem. - Mnacho Echenim:
Pricing in discrete financial models. - Bertram Felgenhauer:
Minsky Machines. - Filip Maric, Mirko Spasic, René Thiemann:
An Incremental Simplex Algorithm with Unsatisfiable Core Generation. - Wenda Li:
The Budan-Fourier Theorem and Counting Real Roots with Multiplicity. - Lawrence C. Paulson:
Quaternions. - Angeliki Koutsoukou-Argyraki:
Octonions. - Walter Guttmann:
Aggregation Algebras. - Manuel Eberl, Lawrence C. Paulson:
The Prime Number Theorem. - Alexander Maletzky:
Signature-Based Gröbner Basis Algorithms. - Manuel Eberl:
Symmetric Polynomials. - Manuel Eberl:
The Transcendence of π. - Friedrich Kurz, Mohammad Abdulaziz:
Upper Bounding Diameters of State Spaces of Factored Transition Systems. - Alexander Bentkamp:
Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms. - Manuel Eberl:
Randomised Binary Search Trees. - Fabian Immler, Bohua Zhan:
Smooth Manifolds. - Asta Halkjær From:
Epistemic Logic. - David Fuenmayor, Christoph Benzmüller:
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL. - Jonas Rädle, Lars Hupel:
Deriving generic class instances for datatypes. - Jonas Keinholz:
Matroids. - Bohua Zhan:
Auto2 Prover. - Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. - Sebastiaan J. C. Joosten:
Graph Saturation. - Georg Struth:
Properties of Orderings and Lattices. - Georg Struth:
Quantales. - Georg Struth:
Transformer Semantics. - Andreas Lochbihler, S. Reza Sefidgar:
Constructive Cryptography in HOL. - Bohua Zhan:
Verifying Imperative Programs using Auto2. - Roy Overbeek:
Formalization of Concurrent Revisions. - Achim D. Brucker, Michael Herzberg:
A Formal Model of the Document Object Model.
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-05-08 21:18 CEST 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:
