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.
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.