![](https://dblp.uni-trier.de./img/logo.320x120.png)
![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 2017
Volume 2017, 2017
- Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen:
First-Order Logic According to Harrison. - Pasquale Noce:
Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method. - Achim D. Brucker, Lukas Brügger, Burkhart Wolff:
Formal Network Models and Their Application to Firewall Policies. - Manuel Eberl:
The Transcendence of e. - Julian Biendarra, Manuel Eberl:
Bertrand's postulate. - Max Wagner, Denis Lohner:
Minimal Static Single Assignment Form. - Lukas Bulwahn, Manuel Eberl:
Bernoulli Numbers. - Joseph Lallemand, Christoph Sprenger
:
Refining Authenticated Key Agreement with Strong Adversaries. - Walter Guttmann:
Stone Relation Algebras. - Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Soundness. - Rose Bohrer:
Differential Dynamic Logic. - Christoph Dittmann:
Menger's Theorem. - Stefan Berghofer:
The Group Law for Elliptic Curves. - Manuel Eberl:
The Euler-MacLaurin Formula. - Manuel Eberl:
Lower bound on comparison-based sorting algorithms. - Manuel Eberl:
The number of comparisons in QuickSort. - Manuel Eberl:
Expected Shape of Random Binary Search Trees. - Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
Subresultants. - Lars Hupel:
Lazifying case constants. - Lars Hupel:
Constructor Functions. - Steven Obua:
Local Lexing. - David Fuenmayor, Christoph Benzmüller:
Types, Tableaus and Gödel's God in Isabelle/HOL. - Eugene W. Stark:
Monoidal Categories. - Simon Wimmer, Peter Lammich:
The Floyd-Warshall Algorithm for Shortest Paths. - Andreas Lochbihler:
CryptHOL. - Andreas Lochbihler, S. Reza Sefidgar, Bhargav Bhatt:
Game-based cryptography in HOL. - Joshua Schneider, Manuel Eberl, Andreas Lochbihler:
Monad normalisation. - Andreas Lochbihler:
Effect polymorphism in higher-order logic. - Andreas Lochbihler:
Probabilistic while loop. - Christoph Sprenger
, Ivano Somaini:
Developing Security Protocols by Refinement. - Simon Foster, Frank Zeyda:
Optics. - Peter Lammich, S. Reza Sefidgar:
Flow Networks and the Min-Cut-Max-Flow Theorem. - Peter Lammich, S. Reza Sefidgar:
Formalizing Push-Relabel Algorithms. - Manuel Eberl:
Buffon's Needle Problem. - Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes, Georg Struth:
Partial Semigroups and Convolution Algebras. - Julius Michaelis, Tobias Nipkow:
Propositional Proof Systems. - Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, Alastair R. Beresford:
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes. - Michael Rawson:
Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus. - Manuel Eberl:
Minkowski's Theorem. - Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel:
HOLCF-Prelude. - Jeremy G. Siek:
Declarative Semantics for Functional Languages. - Diego Marmsoler:
Dynamic Architectures. - Lukas Bulwahn:
Stewart's Theorem and Apollonius' Theorem. - Cristina Matache, Victor B. F. Gomes, Dominic P. Mulligan:
The LambdaMu-calculus. - Tobias Nipkow:
Root-Balanced Tree. - Jonas Rädle:
Orbit-Stabiliser Theorem with Application to Rotational Symmetries. - Julian Parsert, Cezary Kaliszyk:
Microeconomics and the First Welfare Theorem. - Ben Blumson:
Anselm's God in Isabelle/HOL. - Daniel Kirchner:
Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL. - Lars Hupel:
Dictionary Construction. - Walter Guttmann:
Stone-Kleene Relation Algebras. - David Fuenmayor, Christoph Benzmüller:
Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument. - Manuel Eberl:
Dirichlet Series. - Manuel Eberl:
The Hurwitz and Riemann ζ Functions. - Florian Messner, Julian Parsert, Jonas Schöpf, Christian Sternagel:
Homogeneous Linear Diophantine Equations. - Manuel Eberl:
Linear Recurrences. - Wenda Li:
Count the Number of Complex Roots. - Wenda Li:
Evaluate winding numbers through Cauchy indices. - Julian Brunner:
Büchi Complementation. - Julian Brunner:
Transition Systems and Automata. - Peter Gammie, Gianpaolo Gioiosa:
The Kuratowski Closure-Complement Theorem. - Sven Linker:
Hybrid Multi-Lane Spatial Logic. - Tim Jungnickel, Lennart Oldenburg, Matthias Loibl:
The IMAP CmRDT. - René Thiemann:
Stochastic Matrices and the Perron-Frobenius Theorem. - Fabian Hellauer, Peter Lammich:
The string search algorithm by Knuth, Morris and Pratt. - Manuel Eberl:
The Mason-Stother's Theorem. - Manuel Eberl:
The Median-of-Medians Selection Algorithm. - Lukas Bulwahn:
The Falling Factorial of a Sum. - Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Operations on Bounded Natural Functors. - Manuel Eberl:
Dirichlet L-Functions and Dirichlet's Theorem.
![](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.