Stop the war!Остановите войну!
for scientists:
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.
a service of 
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 2023-09-29 23:14 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:
